From 78856dfd7236dbf25d689c8ea9bc2c0105d70b7d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Fri, 28 Aug 2020 15:21:32 +0200
Subject: [PATCH] Add `insert_replicate_strong`.

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

diff --git a/theories/list.v b/theories/list.v
index 3e5964ed..8cf8eb91 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1226,6 +1226,15 @@ Proof.
 Qed.
 Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
 Proof. revert i. induction n; intros [|?]; f_equal/=; auto. Qed.
+Lemma insert_replicate_lt x y n i :
+  i < n →
+  <[i:=y]>(replicate n x) = replicate i x ++ y :: replicate (n - S i) x.
+Proof.
+  revert i. induction n as [|n IH]; [ by lia | ].
+  intros [|i] Hi; simpl.
+  - by rewrite Nat.sub_0_r.
+  - by rewrite IH by lia.
+Qed.
 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.
-- 
GitLab