From f9830af6aa2bb6f1e353b3ebf869721e41b2d2db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 14 Aug 2019 08:55:00 +0200
Subject: [PATCH] Add `replicate_S_end`.

---
 theories/list.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 994917a0..18365ab4 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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.
 Lemma replicate_S n x : replicate (S n) x = x :: replicate  n x.
 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 :
   replicate (n + m) x = replicate n x ++ replicate m x.
 Proof. induction n; f_equal/=; auto. Qed.
-- 
GitLab