proposition: Lemma Exercise4_11h M N: max_pure A R M -> max_pure A R N -> sub (M -s N) (unionb (Lg (N -s M) (fun z => (Ex4_11EM M z)))).
proof: Proof. move => mp np y ymn. have /setC_P[ym yn] := ymn. have yIA : inc y A by have [H _ _] := mp; apply: H. apply/setUb_P1. suff IH : forall K, finite_set K -> (forall M, max_pure A R M -> inc y M -> K = Ex4_11EM N y -s M -> exists2 x : Set, inc x K & inc y (Ex4_11EM M x)). have [] // := (IH (Ex4_11EM N y -s M) _ M). apply: sub_finite_set (_ : sub _ (Ex4_11EM N y +s1 y)) _. by move=> z /setC_P[izeny _]; apply/setU1_P; left. have yan : inc y (A -s N) by apply/setC_P. have [_ rF _ _] := mnr; apply: rF. by move: (Exercise4_11d np yan) => [F0n F0R]. move=> x /setC_P[ixeny nixm] iyemx; exists x => //. apply/setC_P; split => //. have [||senyn _] // := (@Exercise4_11d N y); first by apply/setC_P. by apply: senyn. move=> {M mp ymn ym}. apply: (@finite_set_strong_induction (fun K => forall M : Set, max_pure A R M -> inc y M -> K = Ex4_11EM N y -s M -> exists2 x : Set, inc x K & inc y (Ex4_11EM M x))). move=> K fk IH M mp ym ek. have iya : inc y A by have [sma _ _] := mp; apply: sma. have [x /setC_P[ixeny nixm]] : nonempty (Ex4_11EM N y -s M). apply/nonemptyP => /empty_setC sEm. have /(_ (Ex4_11EM N y +s1 y))[] : pure R M by case: mp. by apply: setU1_sub. have [] // := (@Exercise4_11d _ y np). by apply: setC_i. have ixn : inc x N. have [|senyn _] // := (@Exercise4_11d _ y np); first by apply/setC_P. by apply: senyn. have ixa : inc x A by have [sna _ _] := np; apply: sna. have [y' /setC_P[iy'emx niy'em]] : nonempty (Ex4_11EM M x -s N). apply/nonemptyP => /empty_setC semxn. have [_ pn _] := np; case: (pn ((Ex4_11EM M x +s1 x))). by move=> z /setU1_P[/semxn|->]. case: (@Exercise4_11d _ x mp) => //. by apply/setC_P. have iy'm : inc y' M. have [|semxm _] // := (@Exercise4_11d _ x mp); first by apply/setC_P. by apply: semxm. have dxy' : x <> y' by move=> exy'; case: nixm; rewrite exy'. have [iyemx|niyemx] := inc_or_not y (Ex4_11EM M x). have iym : inc y M. by have [|semxm _] // := (@Exercise4_11d _ x mp); apply/setC_P. exists x => //; rewrite ek. by apply/setC_P. have dyy' : y <> y' by move=> eyy'; case: niyemx; rewrite eyy'. pose M' := (M +s1 x) -s1 y'. have m'p : max_pure A R M'. by apply: Exercise4_11f => //; apply/setC_P. have senym'enym : sub (Ex4_11EM N y -s M') (Ex4_11EM N y -s M). move=> z /setC_P[izeny nizm']; apply/setC_P; split => //. move=> izm; case: (nizm'). apply/setC1_P; split; first by apply/setU1_P; left. move=> ezy'; case: niy'em; rewrite -ezy'. have [|senyn _] := @Exercise4_11d _ y np. by apply/setC_P. by apply: senyn. case: (@IH (Ex4_11EM N y -s M') _ M') => //. - rewrite ek; split => //. move=> eenymenym. have : inc x (Ex4_11EM N y -s M) by apply/setC_P; split => //. rewrite -eenymenym => /setC_P[_ []]. apply/setC_P; split; first by apply/setU1_1. by move=> /set1_eq . - apply/setC1_P; split => //. by apply/setU1_P; left. move=> x' /setC_P[ix'exny nix'm'] iyem'x'. have nix'm : ~ inc x' M. suff : inc x' (Ex4_11EM N y -s M) by case/setC_P. by apply/senym'enym/setC_P. have ix'N : inc x' N. have [|senyn _] := @Exercise4_11d _ y np; first by apply/setC_P. by apply: senyn. have ix'A : inc x' A by have [sna _ _] := np; apply: sna. have iym' : inc y M'. have [|sem'x'm' _] := @Exercise4_11d _ x' m'p; first by apply/setC_P. by apply: sem'x'm'. have [iy'emx'|niy'emx'] := inc_or_not y' (Ex4_11EM M x'); last first. have smx'm' : sub (Ex4_11EM M x') M'. move=> z izemx'. apply/setC1_P; split => //; last first. by move=> ezy'; case: niy'emx'; rewrite -ezy'. apply/setU1_P; left. have [|semx'm _] := @Exercise4_11d _ x' mp. by apply/setC_P. by apply: semx'm. exists x' => //. rewrite ek. by apply/senym'enym/setC_P. suff <-: Ex4_11EM M' x' = Ex4_11EM M x' by []. apply/sym_equal/Exercise4_11d' => //. - by apply/setC_P. - move=> z izemx'. have [sma _ _ ] := mp; apply: sma. have [|semx'm _] := @Exercise4_11d _ x' mp; first by apply/setC_P. by apply: semx'm. by have [] // := @Exercise4_11d _ x' mp; apply/setC_P. have iy' : inc y' ((Ex4_11EM M x +s1 x) \cap (Ex4_11EM M x' +s1 x')). by apply/setI2_P; split; apply/setU1_P; left. have dxx' : x <> x'. move=> exx'; case: nix'm'; rewrite -exx'. apply/setC1_P; split; first by apply/setU1_P; right. move=> exy'; case: nix'm. by rewrite -exx' exy'. have [_ _ mr _] := mnr. red in mr. case: (mr (Ex4_11EM M x +s1 x) (Ex4_11EM M x' +s1 x') _ _ _ y') => //. - by case: (@Exercise4_11d M x) => //; apply/setC_P. - by case: (@Exercise4_11d M x') => //; apply/setC_P. - move=> eemxxemx'x'. have : inc x (Ex4_11EM M x +s1 x) by apply/setU1_P; right. rewrite eemxxemx'x' => /setU1_P[] // ixmx'. case: nixm. case: (@Exercise4_11d M x') => //; first by apply/setC_P. by move=> /(_ _ ixmx'). move=> X [ixr sxc niy'x]. have sxm'x' : sub X (M' +s1 x'). move=> z izx. case/setU2_P: (sxc _ izx); last first. case/setU1_P=> [izemx'|->]; last by apply/setU1_P; right. apply/setU1_P; left. apply/setC1_P; split; last first. by move=> ezy'; case: niy'x; rewrite -ezy'. apply/setU1_P; left. case: (@Exercise4_11d M x') => //; first by apply/setC_P. by move=> /(_ _ izemx'). move=> /setU1_P[|->]; last first. apply/setU1_P; left. apply/setC1_P; split => //. by apply/setU1_P; right. move=> izemx. apply/setU1_P; left. apply/setC1_P; split; last first. by move=> ezy'; case: niy'x; rewrite -ezy'. apply/setU1_P; left. case: (@Exercise4_11d M x) => //; first by apply/setC_P. by move=> /(_ _ izemx). have ix'x : inc x' X. ex_middle nix'x. have [_ pm' _] := m'p. case: (pm' X) => //. move=> z izx. have /setU1_P[|ezx] // := sxm'x' _ izx. by case: nix'x; rewrite -ezx. have exem'x' : X -s1 x' = Ex4_11EM M' x'. apply: Exercise4_11d' => //. - by apply/setC_P. - move => z /setC1_P[izx _]. by case: mnr => /(_ _ ixr _ izx). move=> z /setC1_P[izx' dzx']. by have /setU1_P[|ezx'] := sxm'x' _ izx'. by rewrite setC1_K. suff : inc y ((Ex4_11EM M x +s1 x) \cup (Ex4_11EM M x' +s1 x')). case/setU2_P; case/setU1_P. - by move=> iymx; exists x. - by move=> eyx; case: yn; rewrite eyx. - move=> iymx; exists x' => //. by rewrite ek; apply/setC_P. by move=> eyx'; case: yn; rewrite eyx'. apply: sxc. rewrite -(@setC1_K X x') // exem'x'. by apply/setU1_P; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)