Commit f9830af6 authored by Robbert Krebbers's avatar Robbert Krebbers

Add `replicate_S_end`.

parent 6827b242
Pipeline #19056 failed with stage
in 0 seconds
...@@ -1155,6 +1155,8 @@ Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y. ...@@ -1155,6 +1155,8 @@ Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed. Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x. Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed. Proof. done. Qed.
Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
Proof. induction n; f_equal/=; auto. Qed.
Lemma replicate_plus n m x : Lemma replicate_plus n m x :
replicate (n + m) x = replicate n x ++ replicate m x. replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; f_equal/=; auto. Qed. Proof. induction n; f_equal/=; auto. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment