Some list related lemmas

Some more lemmas that I proved for my development.

theories/list.v

@@ -565,6 +565,9 @@ Lemma list_insert_id l i x : l !! i = Some x → <[i:=x]>l = l.
 Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. Qed.
 Lemma list_insert_ge l i x : length l ≤ i → <[i:=x]>l = l.
 Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
+Lemma list_insert_insert l i x y:
+  <[i := x]> (<[i := y]> l) = <[ i:= x]> l.
+Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed.
 
 Lemma list_lookup_other l i x :
   length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
@@ -955,6 +958,11 @@ Proof.
 Qed.
 Lemma take_nil n : take n [] =@{list A} [].
 Proof. by destruct n. Qed.
+Lemma take_S_r l n x: l !! n = Some x → take (S n) l = take n l ++ [x].
+Proof.
+  revert n. induction l as [|e l IH]; [done |]. intros n.
+  destruct n; naive_solver eauto with f_equal.
+Qed.
 Lemma take_app l k : take (length l) (l ++ k) = l.
 Proof. induction l; f_equal/=; auto. Qed.
 Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l.
@@ -1012,6 +1020,9 @@ Lemma drop_0 l : drop 0 l = l.
 Proof. done. Qed.
 Lemma drop_nil n : drop n [] =@{list A} [].
 Proof. by destruct n. Qed.
+Lemma drop_S l x n:
+  l !! n = Some x → drop n l = x :: drop (S n) l.
+Proof. revert n. induction l as [|e l IH]; [done|]. intros n. destruct n; naive_solver. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l ≤ n → drop n l = [].
@@ -1110,6 +1121,9 @@ Proof. done. Qed.
 Lemma replicate_plus n m x :
   replicate (n + m) x = replicate n x ++ replicate m x.
 Proof. induction n; f_equal/=; auto. Qed.
+Lemma replicate_cons_app n x:
+  x :: replicate n x = replicate n x ++ [x].
+Proof. induction n; f_equal/=; eauto.  Qed.
 Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
 Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
 Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
@@ -3644,6 +3658,18 @@ Section zip.
     rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1.
     induction Hlk2; intros ?? [|??????]; simpl; auto.
   Qed.
+
+  Lemma elem_of_zip_1 x1 x2 l k:
+    (x1, x2) ∈ zip l k → x1 ∈ l.
+  Proof.
+    revert k. induction l; intros [|]; simpl; inversion_clear 1; rewrite elem_of_cons; naive_solver.
+  Qed.
+
+  Lemma elem_of_zip_2 x1 x2 l k:
+    (x1, x2) ∈ zip l k → x2 ∈ k.
+  Proof.
+    revert l. induction k; intros [|]; simpl; inversion_clear 1; rewrite elem_of_cons; naive_solver.
+  Qed.
 End zip.
 
 Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :