From 09111a5795dda4827c3b9f1f61453cd35ea1ae48 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 3 May 2021 18:35:51 +0200
Subject: [PATCH] add insert_take_drop

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

diff --git a/theories/list.v b/theories/list.v
index 07bd5a51..1887fb48 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1192,6 +1192,17 @@ Proof.
   revert n m. induction l; intros [|?] [|?] ?;
     f_equal/=; auto using take_drop with lia.
 Qed.
+Lemma insert_take_drop l i x :
+  i < length l →
+  <[i:=x]> l = take i l ++ x :: drop (S i) l.
+Proof.
+  intros Hi.
+  rewrite <-(take_drop_middle (<[i:=x]> l) i x).
+  2:{ by rewrite list_lookup_insert. }
+  rewrite take_insert by done.
+  rewrite drop_insert_gt by lia.
+  done.
+Qed.
 
 Lemma app_eq_inv l1 l2 k1 k2 :
   l1 ++ l2 = k1 ++ k2 →
-- 
GitLab