diff --git a/theories/list.v b/theories/list.v
index 3e5964ede7e63f315b3f89ca8648b865d40fdd88..8cf8eb91304e0836740494ebaf9f40a13501cad7 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.