proposition: Lemma Add_commutative : forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
proof: Proof. intros A x y. unfold Add. rewrite (Union_associative A (Singleton U x) (Singleton U y)). rewrite (Union_commutative (Singleton U x) (Singleton U y)). rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset