diff --git a/theories/collections.v b/theories/collections.v
index cf898767d00da9410bb3cd05161a0cc96b9ad773..a42ef825bbf101f2ce84d48faf4a43e879e204c8 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -339,6 +339,11 @@ Section simple_collection.
   Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
   Proof. set_solver. Qed.
 
+  Lemma union_cancel_l X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X ≡ Z ∪ Y → X ≡ Y.
+  Proof. set_solver. Qed.
+  Lemma union_cancel_r X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z ≡ Y ∪ Z → X ≡ Y.
+  Proof. set_solver. Qed.
+
   (** Empty *)
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. set_solver. Qed.
@@ -455,6 +460,11 @@ Section simple_collection.
     Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
     Proof. unfold_leibniz. apply empty_union. Qed.
 
+    Lemma union_cancel_l_L X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X = Z ∪ Y → X = Y.
+    Proof. unfold_leibniz. apply union_cancel_l. Qed.
+    Lemma union_cancel_r_L X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z = Y ∪ Z → X = Y.
+    Proof. unfold_leibniz. apply union_cancel_r. Qed.
+
     (** Empty *)
     Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X.
     Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.