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