diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 67d77eaf7780b6d01cf8f9a9963b7c0a6729f830..c861db2d355ccbe3df2e1b40c1683f255a51e475 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2107,11 +2107,18 @@ Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
 Proof. apply delete_union_with. Qed.
 Lemma delete_insert_union {A} (m1 m2 : M A) i x :
-  m1 !! i = Some x ->
-  delete i m1 ∪ <[i := x]> m2 = m1 ∪ m2.
+  m1 !! i = Some x →
+  delete i m1 ∪ <[i:=x]> m2 = m1 ∪ m2.
 Proof.
-  intros Hmi. rewrite <-insert_union_r by apply lookup_delete.
-  rewrite insert_union_l, insert_delete, insert_id; done.
+  intros. rewrite <-insert_union_r by apply lookup_delete.
+  by rewrite insert_union_l, insert_delete, insert_id by done.
+Qed.
+Lemma insert_delete_union {A} (m1 m2 : M A) i x :
+  m1 !! i = None → m2 !! i = Some x →
+  <[i:=x]> m1 ∪ delete i m2 = m1 ∪ m2.
+Proof.
+  intros. rewrite <-insert_union_l by apply lookup_delete.
+  by rewrite insert_union_r, insert_delete, insert_id by done.
 Qed.
 Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
   map_Forall P (m1 ∪ m2) → map_Forall P m1.