proposition: Theorem Union_add : forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
proof: Proof. unfold Add; auto using Union_associative with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset