proposition: Lemma Included_Add : forall (X A:Ensemble U) (x:U), Included U X (Add U A x) -> Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
proof: Proof. intros X A x H'0; try assumption. elim (classic (In U X x)). - intro H'1; right; try assumption. exists (Subtract U X x). split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets. red in H'0. red. intros x0 H'2; try assumption. lapply (Subtract_inv U X x x0); auto with sets. intro H'3; elim H'3; intros K K'; clear H'3. lapply (H'0 x0); auto with sets. intro H'3; try assumption. lapply (Add_inv U A x x0); auto with sets. intro H'4; elim H'4; [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. elim K'; auto with sets. - intro H'1; left; try assumption. red in H'0. red. intros x0 H'2; try assumption. lapply (H'0 x0); auto with sets. intro H'3; try assumption. lapply (Add_inv U A x x0); auto with sets. intro H'4; elim H'4; [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ]. absurd (In U X x0); auto with sets. rewrite <- H'5; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets