The Couple operation is commutative

Columbus240 · Columbus240 · commit 4bcc696e6730 · 2021-08-31T20:02:16.000+02:00
diff --git a/theories/ZornsLemma/Powerset_facts.v b/theories/ZornsLemma/Powerset_facts.v
@@ -117,3 +117,9 @@ Proof.
   { constructor. }
   destruct (classic (In U x)); [right|left]; assumption.
 Qed.
+
+Lemma Couple_swap X (x y : X) :
+  Couple x y = Couple y x.
+Proof.
+  extensionality_ensembles_inv; constructor.
+Qed.
