diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e40137dfcecdf66da09fc0e53f6853c712e788d1..b720debf960a99d1c7d52e3f2947fed49079af20 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2446,12 +2446,15 @@ Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
 Lemma insert_difference {A} (m1 m2 : M A) i x :
-  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
+  <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ delete i m2.
 Proof.
   intros. apply map_eq. intros j. apply option_eq. intros y.
-  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some, lookup_delete_None.
   naive_solver.
 Qed.
+Lemma insert_difference' {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
+Proof. intros. by rewrite insert_difference, delete_notin. Qed.
 Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 :
   <[i := x1]> m1 ∖ <[i := x2]> m2 = m1 ∖ <[i := x3]> m2.
 Proof.