Add insert delete lemma for big ops over gmap

theories/algebra/big_op.v

@@ -323,6 +323,12 @@ Section gmap.
     by apply big_opL_proper=> ? [??].
   Qed.
 
+  Lemma big_opM_insert_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
+    ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
+  Proof.
+    rewrite -insert_delete big_opM_insert; first done. by rewrite lookup_delete.
+  Qed.
+
   Lemma big_opM_insert_override (f : K → A → M) m i x x' :
     m !! i = Some x → f i x ≡ f i x' →
     ([^o map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([^o map] k↦y ∈ m, f k y).

theories/bi/big_op.v

@@ -789,6 +789,10 @@ Section map.
     ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
   Proof. apply big_opM_delete. Qed.
 
+  Lemma big_sepM_insert_delete Φ m i x :
+    ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
+  Proof. apply big_opM_insert_delete. Qed.
+
   Lemma big_sepM_insert_2 Φ m i x :
     TCOr (∀ x, Affine (Φ i x)) (Absorbing (Φ i x)) →
     Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y) -∗ [∗ map] k↦y ∈ <[i:=x]> m, Φ k y.
@@ -1080,6 +1084,14 @@ Section map2.
       by rewrite map_lookup_zip_with Hx1 Hx2.
   Qed.
 
+  Lemma big_sepM2_insert_delete Φ m1 m2 i x1 x2 :
+    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
+    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2.
+  Proof.
+    rewrite -(insert_delete m1) -(insert_delete m2).
+    apply big_sepM2_insert; by rewrite lookup_delete.
+  Qed.
+
   Lemma big_sepM2_insert_acc Φ m1 m2 i x1 x2 :
     m1 !! i = Some x1 → m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢