diff --git a/theories/collections.v b/theories/collections.v
index a37e13658724a2ac2ef867052420a4e79ec00894..28a8f25b3eeb2cf405414ab52f22432bff71e1ee 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -346,7 +346,6 @@ Section simple_collection.
   Proof. set_solver. Qed.
   Lemma elem_of_union_r x X Y : x âˆˆ Y â†’ x âˆˆ X âˆª Y.
   Proof. set_solver. Qed.
-
   Lemma union_preserving_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆª Y1 âŠ† X âˆª Y2.
   Proof. set_solver. Qed.
   Lemma union_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆª Y âŠ† X2 âˆª Y.
@@ -613,6 +612,14 @@ Section collection.
   Lemma difference_disjoint X Y : X âŠ¥ Y â†’ X âˆ– Y â‰¡ X.
   Proof. set_solver. Qed.
 
+  Lemma difference_preserving X1 X2 Y1 Y2 :
+    X1 âŠ† X2 â†’ Y2 âŠ† Y1 â†’ X1 âˆ– Y1 âŠ† X2 âˆ– Y2.
+  Proof. set_solver. Qed.
+  Lemma difference_preserving_l X Y1 Y2 : Y2 âŠ† Y1 â†’ X âˆ– Y1 âŠ† X âˆ– Y2.
+  Proof. set_solver. Qed.
+  Lemma difference_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆ– Y âŠ† X2 âˆ– Y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma disjoint_intersection X Y : X âŠ¥ Y â†” X âˆ© Y â‰¡ âˆ….
   Proof. set_solver. Qed.