diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0197e848621119394e6218975baf60b339fc0308..48aae385833f66d4077b8a72b3fce07e026f4b2d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2422,6 +2422,8 @@ Proof.
 Qed.
 Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
+Lemma map_difference_subseteq {A} (m1 m2 : M A) : m1 ∖ m2 ⊆ m1.
+Proof. apply map_subseteq_spec. by intros ?? []%lookup_difference_Some. Qed.
 Lemma map_difference_union {A} (m1 m2 : M A) :
   m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
 Proof.
@@ -2441,6 +2443,21 @@ Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
+Lemma map_difference_insert_l {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> m1 ∖ m2 = <[i := x]> (m1 ∖ m2).
+Proof.
+  intros. apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some.
+  naive_solver.
+Qed.
+Lemma map_difference_insert_subseteq {A} (m1 m2 : M A) i x :
+  <[i := x]> m1 ∖ <[i := x]> m2 ⊆ m1 ∖ m2.
+Proof.
+  apply map_subseteq_spec. intros i' x'.
+  rewrite !lookup_difference_Some, lookup_insert_Some, lookup_insert_None.
+  naive_solver.
+Qed.
+
 Lemma delete_difference {A} (m1 m2 : M A) i x :
   delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
 Proof.