proposition: Theorem covers_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 H'1; try assumption. elim (setcover_inv A a a'); auto with sets. intros H'6 H'7. clear H'1. elim (Strict_Included_inv U a a'); auto with sets. intros H'5 H'8; elim H'8. intros x H'1; elim H'1. intros H'2 H'3; try assumption. exists x. split; [ try assumption | idtac ]. - clear H'8 H'1. elim (H'7 (Add U a x)); auto with sets. + intro H'1. absurd (a = Add U a x); auto with sets. red; intro H'8; try exact H'8. apply H'3. rewrite H'8; auto with sets. + auto with sets. red. intros x0 H'1; elim H'1; auto with sets. intros x1 H'8; elim H'8; auto with sets. - split; [ idtac | try assumption ]. red in H'0; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets