proposition: Theorem covers_is_Add : forall A a a':Ensemble U, Included U a A -> Included U a' A -> (covers (Ensemble U) (Power_set_PO U A) a' a <-> (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
proof: Proof. intros A a a' H' H'0; split; intro K. - apply covers_Add with (A := A); auto with sets. - elim K. intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1. apply Add_covers; intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets