diff --git a/theories/collections.v b/theories/collections.v
index 27e683054cd68a43f970a6d889325ecee66d9d22..888be9b6503e9b41b8c2a83e5e4528febd2a0c6d 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -418,7 +418,7 @@ Section collection.
   Proof. set_solver. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
   Proof. set_solver. Qed.
-  Lemma disjoint_union_difference X Y : X ⊥ Y → (X ∪ Y) ∖ X ≡ Y.
+  Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X.
   Proof. set_solver. Qed.
 
   Section leibniz.
@@ -438,8 +438,8 @@ Section collection.
     Lemma difference_intersection_distr_l_L X Y Z :
       (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
     Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
-    Lemma disjoint_union_difference_L X Y : X ⊥ Y → (X ∪ Y) ∖ X = Y.
-    Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
+    Lemma difference_disjoint_L X Y : X ⊥ Y → X ∖ Y = X.
+    Proof. unfold_leibniz. apply difference_disjoint. Qed.
   End leibniz.
 
   Section dec.