proposition: Theorem Add_covers : forall A a:Ensemble U, Included U a A -> forall x:U, In U A x -> ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
proof: Proof. intros A a H' x H'0 H'1; try assumption. apply setcover_intro; auto with sets. - red. split; [ idtac | red; intro H'2; try exact H'2 ]; auto with sets. apply H'1. rewrite H'2; auto with sets. - red; intro H'2; elim H'2; clear H'2. intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. lapply (Strict_Included_inv U a z); auto with sets; clear H'3. intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5. intros x0 H'2; elim H'2. intros H'5 H'6; try assumption. generalize H'4; intro K. red in H'4. elim H'4; intros H'8 H'9; red in H'8; clear H'4. lapply (H'8 x0); auto with sets. intro H'7; try assumption. elim (Add_inv U a x x0); auto with sets. intro H'15. cut (Included U (Add U a x) z). + intro H'10; try assumption. red in K. elim K; intros H'11 H'12; apply H'12; clear K; auto with sets. + rewrite H'15. red. intros x1 H'10; elim H'10; auto with sets. intros x2 H'11; elim H'11; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets