diff --git a/prelude/collections.v b/prelude/collections.v index 39eb6f1033adbbdbd37e69f16249ad868fa30dec..15920610ad97a7d7edab3f16ee69e7b036720262 100644 --- a/prelude/collections.v +++ b/prelude/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.