proposition: Lemma Add_distributes : forall (A B:Ensemble U) (x y:U), Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
proof: Proof. intros A B x y H'; try assumption. rewrite <- (Union_add (Add U A x) B y). unfold Add at 4. rewrite (Union_commutative A (Singleton U x)). rewrite Union_associative. rewrite (Union_absorbs A B H'). rewrite (Union_commutative (Singleton U x) A). auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset