proposition: Lemma exercise6_11b4 E X (R := exercise6_11b_rel X) (p1 := fun u => (exists a b, [/\ a<> b, R a b & u = Zo E (fun x => R a x /\ R b x)])) (p2:= fun u => (exists x, [/\ u = singleton x, inc x E & forall y, inc y E -> R x y -> x = y])) (p3:= fun u => (exists v, [/\ inc v X, u <> v, sub u v & singletonp u])): exercise6_11b_assumption X E -> [/\ (forall u, inc u X -> p1 u \/ p2 u \/ p3 u ), (forall u, p1 u -> inc u X) & (forall u, p2 u -> inc u X)].
proof: Proof. move => [uXE alne i2 i3]; split. move=> u uX. case: (p_or_not_p (singletonp u)) => su. right; case: (p_or_not_p (p3 u)) => p3u; first by right. left; move: (su) => [x sx]. rewrite sx; exists x; split => //. rewrite -uXE; apply: (@setU_i _ u) =>//; rewrite sx; fprops. move=> y yE Rxy; case: (equal_or_not x y) =>//. move=> xy; move: Rxy=> [A [AX xA yA]]. case p3u; exists A; split =>//. by dneg uA; move: yA; rewrite -uA sx;move /set1_P. by move=> t; rewrite sx; move/set1_P => ->. constructor 1; red. move: (alne _ uX) => [y yu]; exists y. case (p_or_not_p (exists2 v, inc v u & v <> y)). move=> [x xu xy]; exists x;split; [auto | by exists u |]. set_extens w. move=> wu; apply: Zo_i. rewrite - uXE; apply: (@setU_i _ u) =>//. split;exists u; split => //. move /Zo_P=> [wE [ [A [AX xA yA]] [A' [AX' xA' yA']]]]. case: (equal_or_not A u)=> Au; first by rewrite -Au. case: (equal_or_not A' u)=> Au'; first by rewrite -Au'. have xi: (inc x (u \cap A')) by fprops. have yi: (inc y (u \cap A)) by fprops. case: (equal_or_not A A') => AA'. case: (i2 _ _ uX AX)=> aux. by case: Au'; rewrite -AA' aux. rewrite -AA' in xi. by case: xy; apply:(aux _ _ xi yi). move: (i3 _ _ _ AX AX' uX). case =>//; case =>//; case =>//. case; first by move=> h; empty_tac1 w; aw. case; first by move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 x; aw. move=> [h1 h2]. rewrite setI2_C -h2 in xi. rewrite setI2_C -h1 in yi. case: (i2 _ _ AX AX')=>// aux. case: xy; by apply: (aux _ _ xi yi). move=> h;case: su; exists y; apply: set1_pr1; first by ex_tac. move => w wu;case: (equal_or_not w y) =>// wy; by case: h; ex_tac. move=> u [a [b [nab [A [AX aA bA]] uZ]]]. suff: (u = A) by move=> ->. rewrite uZ; set_extens t. move /Zo_P=> [tE [[A' [AX' aA' bA']]] [A'' [AX'' aA'' bA'']]]. case: (equal_or_not A A'')=> AA''; first by ue. case: (equal_or_not A A')=> AA'; first by ue. have aAA: inc a (A \cap A') by fprops. have bAA: inc b (A \cap A'') by fprops. case: (equal_or_not A' A'') => aux. case: (i2 _ _ AX AX')=> // ss. rewrite -aux in bAA; case: nab; apply: (ss _ _ aAA bAA). case: (i3 _ _ _ AX AX' AX'') =>//; case =>//; case =>//. case; first by move=> h; empty_tac1 a; aw. case; first by move=> h; empty_tac1 b; aw. case; first by move=> h; empty_tac1 t; aw. move=> [h1 h2]; rewrite - h1 in bAA. case: (i2 _ _ AX AX')=>// ss. case: nab; by apply: (ss _ _ aAA bAA). move=> tA; apply: Zo_i. rewrite -uXE;apply: (@setU_i _ A)=>//. by split;exists A. move=> u [v [uv vE su]]. move: vE;rewrite -uXE; move/setU_P=> [y vy yX]. suff: u = y by move=> ->. rewrite uv; symmetry; apply:set1_pr => // t tv. symmetry;apply: su. rewrite -uXE;apply: (@setU_i _ y) =>//. by exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)