proposition: Lemma Exercise4_5d r k: order r -> natp k -> order_width r k -> Exercise4_5_conc r k.
proof: Proof. move=> or kN; move: k kN r or. apply:Nat_induction. move=> r or [hyp1 hyp2]; exists emptyset. case: (emptyset_dichot (substrate r)). move => ->; rewrite cardinal_set0; split => //. split; last by move=> a /in_set0. split; first by apply: setU_0. by move=> a b /in_set0. by move=> x /in_set0. move=> [x sxr]. have px: inc (singleton x) (free_subsets r). apply: Zo_i; first by apply /setP_P; apply: set1_sub. by move=> u v /set1_P -> /set1_P ->. move:(hyp2 _ px); rewrite cardinal_set1 => h. by move: (cle0 h) => h1; case: card1_nz. move=> k kN hrec r or [[X0 X0f cX0] gensiz]. pose comp C := ((substrate r) -s C). pose indC C := induced_order r ((substrate r) -s C). suff: exists2 C, inc C (total_suborders r) & (forall T, sub T (comp C) -> (free_subset r T) ->(cardinal T) <=c k). move=> [C /total_subordersP [Cs torC ]h1]. set E1 := comp C. have s1: sub E1 (substrate r) by apply: sub_setC. set r1:= indC C. move: (iorder_osr or s1) => [or1 sr1]. have p1: forall x, inc x (free_subsets r1) -> (cardinal x) <=c k. move => x /free_subsetsP[p1 p2]. have p3: free_subset r x. move=> u v ux vx uv; apply:p2 =>//;rewrite /r1 /indC -/(comp C) -/E1 - sr1. by apply /iorder_gle0P => //; apply: p1. rewrite sr1 in p1;exact: (h1 _ p1 p3). move/free_subsetsP: X0f => [X0sr Xfree]. have i1: inc (X0 \cap E1) (free_subsets r1). apply/free_subsetsP; split; first by rewrite sr1; apply: subsetI2r. by move=> x y /setI2_P[x0 xE1] /setI2_P[y0 yE1]/iorder_gle1 xy;apply:Xfree. case: (emptyset_dichot C) => neC. move: (p1 _ i1). have ->: X0 \cap E1 = X0 by rewrite /E1 /comp neC setC_0; apply/setI2id_Pl. rewrite cX0 => /cleNgt; case; exact:(cltS kN). have hrec1: order_width r1 k. split => //; exists (X0 \cap E1) => //. move: (p1 _ i1) => rel1; ex_middle q. have : (cardinal (X0 \cap E1)) <c k by split. have c1: sub (X0 \cap E1) X0 by apply: subsetI2l. move:(cardinal_setC c1); rewrite cX0 /cdiff. set a := cardinal _; set b := cardinal _. have skN: natp (csucc k) by fprops. have ca: cardinalp a by rewrite /a; fprops. have cb: cardinalp b by rewrite /b; fprops. have csa: cardinalp (csucc a) by apply: CS_succ. move => p2; rewrite -p2 in skN. move: (NS_in_sumr cb skN) (NS_in_suml ca skN) => bN aN. move/ (cleSltP aN) /(cleSSP csa (CS_nat kN)). rewrite -p2 (csucc_pr4 csa) (csucc_pr4 ca) - csumA. rewrite csum_11 => p3. move: (csum_le2l aN NS2 bN p3) => /cle2P [x1 [x2 [x1b x2b x12]]]. move: x1b x2b => /setC_P [x10] /setI2_P e1 /setC_P [x20] /setI2_P e2. move: (X0sr _ x10) (X0sr _ x20) => x1s x2s. case: (inc_or_not x1 C)=> x1C; last by case: e1; split => //; apply /setC_P. case: (inc_or_not x2 C)=> x2C; last by case: e2; split => //; apply /setC_P. move: torC => [_ ]; rewrite iorder_sr//; move => tc. case: (tc _ _ x1C x2C) => h; move: (iorder_gle1 h) => aux. by case: x12; move: (Xfree _ _ x10 x20 aux). by case: x12; move: (Xfree _ _ x20 x10 aux). move: (hrec _ or1 hrec1) => [Y [[[uY adi] ane] cY altY]]. set X:= Y +s1 C. have nCY : ~ (inc C Y). move=> CY; move: (ane _ CY) => [x xC]. have : inc x (union Y) by union_tac. by rewrite uY sr1 => /setC_P [_ []]. move: (csucc_pr nCY); rewrite cY -/X => p3. have pr1: union X = substrate r. rewrite /X;set_extens t. move=> /setU_P [y ty /setU1_P]; case => yy; last by apply: Cs; ue. apply: s1; rewrite - sr1 -uY; union_tac. move=> tsr; apply /setU_P;case: (inc_or_not t C) => tC. by exists C;fprops. have : inc t (union Y) by rewrite uY sr1; apply /setC_P. move /setU_P=> [y ty yY]; exists y; fprops. have pr2:disjoint_set X. move=> a b; case /setU1_P => aY; case /setU1_P => bY. + by apply: adi. + right; rewrite bY; apply: disjoint_pr => u uA. have:inc u (union Y) by union_tac. by rewrite uY sr1 => /setC_P [_ nxc]. + right; rewrite aY; apply: disjoint_pr => u uA uB. have:inc u (union Y) by union_tac. by rewrite uY sr1 => /setC_P [_ nxc]. + by left; rewrite aY bY. have pr3: alls X nonempty. by move=> a; case /setU1_P => ay; [ apply: ane | ue ]. exists X; rewrite /partition_s; split => //. move => x; case /setU1_P => aY; apply/total_subordersP; last by ue. move /total_subordersP: (altY _ aY) =>[]; rewrite iorder_sr // => xe1. move: (sub_trans xe1 s1). by rewrite /r1 /indC iorder_trans. pose sra F X := [/\ (cardinal X) <=c (csucc k), partition_w X F & sub X (total_suborders r)]. pose sr C := sub C (substrate r) /\ forall F, finite_set F -> sub F (substrate r) -> exists2 X, sra F X & exists2 Y, inc Y X & sub (C \cap F) Y. set ssr:= Zo (\Po (substrate r)) sr. set sso:= sub_order ssr. move: (sub_osr ssr) => [osso sssr]. have sre: (sr emptyset). split; first by fprops. move=> F Fsf Fsr. set r1:= induced_order r F. move: (iorder_osr or Fsr) => [pa pb]. have fsr1: finite_set (substrate r1) by ue. have fk: forall x, inc x (free_subsets r1) -> (cardinal x) <=c (csucc k). move=> x /free_subsetsP[xr1 fs1]; rewrite pb in xr1. apply: gensiz; apply/free_subsetsP; split. by apply: (@sub_trans F). by move=> u v ux vx uv; apply: fs1 => //; apply/iorder_gle0P => //;apply: xr1. have skN: natp (csucc k) by fprops. case: (emptyset_dichot F) => eF. have pr1:sra F (singleton emptyset). rewrite /sra cardinal_set1 /partition_w eF setU_1; split => //. apply: cge1; fprops; apply: succ_nz. by split => // a b /set1_P -> /set1_P ->; left. have s1: sub emptyset (substrate r) by fprops. move: (iorder_osr or s1) => [pax pbx]. move=> a /set1_P ->; apply/total_subordersP; split => //. by split; fprops; rewrite iorder_sr//; move=> x y /in_set0. exists (singleton emptyset) => //. by exists emptyset; fprops; move => t /setI2_P; case. move: (order_width_exists fsr1) => [mN' mbd' mp']. move: (Exercise4_5b fsr1 pa mN' mp') => [X [[px1 _] xb xc]]; exists X. split => //;[ by rewrite xb; move: (proj1 mp') =>[y /fk ya <-] | ue | ]. by apply: (sub_trans xc); apply:sub_total_suborders1. move: eF => [u]; rewrite - pb - (proj1 px1) => /setU_P [y uy yX]. by ex_tac; move=> t/setI2_P [] /in_set0. have isso: inductive sso. move=> X sX tio;rewrite sssr in sX. set uX:= union X. have uXr: sub uX (substrate r). apply: setU_s2 => y yX t ty. move: (sX _ yX) => /Zo_P [] /setP_P ysr _; apply: (ysr _ ty). suff uxs: inc (union X) ssr. exists (union X); hnf; rewrite sssr; split => //. by move=> y yX; apply /sub_gleP;split;fprops;apply: setU_s1. apply: Zo_i; [ by apply /setP_P | split => //]. move => F fsF Fsr; set w := ((union X) \cap F). case: (emptyset_dichot w) => wne. move: sre; move=> [_ h]; move: (h _ fsF Fsr). have -> // : emptyset \cap F = w. by rewrite wne; apply /set0_P; move=> y /setI2_P [/in_set0]. pose f x:= choose (fun y => inc x y /\ inc y X). have fp: forall x, inc x w -> (inc x (f x) /\ inc (f x) X). move=> x /setI2_P [] /setU_P [y p1 p2] _. by apply choose_pr; exists y. set w1:= fun_image w f. move: (sub_finite_set (@subsetI2r (union X) F) fsF) => fsw. move: (finite_fun_image f fsw); rewrite -/w -/w1 => fsw1. have sw1: sub w1 X. by move => t /funI_P [z zw ->]; case: (fp _ zw). have w1ne : nonempty w1. move: wne => [x xw]; exists (f x); apply /funI_P; ex_tac. have sis: substrate (induced_order sso X) = X by rewrite iorder_sr//; ue. move: (sw1); rewrite - sis => sw2. move: sX; rewrite - sssr => sw3. move: (sub_trans sw1 sw3) => sw4. move: (finite_subset_torder_greatest tio fsw1 w1ne sw2) => [x]. rewrite iorder_trans //; move=> []; rewrite iorder_sr // => xw1 xle. move: (sw1 _ xw1) => xX. have ->: w = x \cap F. set_extens t. move=> tw; apply /setI2_P. have ft: inc (f t) w1 by apply /funI_P; ex_tac. move: (xle _ ft) => /(iorder_gle0P _ ft xw1) /sub_gleP [fts xsr ftx]. move: (fp _ tw) => [pa pb]; split; first by apply: (ftx _ pa). by apply: (@setI2_2 (union X)). move=> /setI2_P[pa pb]; apply /setI2_P;split => //; union_tac. move: (sw3 _ xX); rewrite sssr;move => /Zo_P [_ [_ ok]]. apply: (ok F fsF Fsr). move: (Zorn_lemma osso isso) => [C [Cs Cm]]. move: Cs; rewrite sssr => Cs1; move: (Cs1) => /Zo_P [_ [cp1 cp2]]. have toc: inc C (total_suborders r). move: (iorder_osr or cp1) => [pax pbx]. apply:(total_suborder_prop or cp1) => x y xC yC; hnf. set F:= doubleton x y. have fsF: finite_set F by apply: set2_finite. have FC:sub F C by apply: sub_set2. have Fsr: sub F (substrate r) by apply: sub_trans cp1. move: (cp2 _ fsF Fsr) => [X [pa pb pc]] [Y YX si]. move /total_subordersP:(pc _ YX) => [ysr [ory]]; rewrite iorder_sr //. have xY: inc x Y by apply: si; apply /setI2_P;rewrite /F;split;fprops. have yY: inc y Y by apply: si; apply /setI2_P;rewrite /F;split;fprops. move=> aux; case: (aux _ _ xY yY) => aux2; move: (iorder_gle1 aux2); fprops. case: (p_or_not_p (forall T, sub T (comp C) -> free_subset r T -> (cardinal T) <=c k)) => hh. by exists C. case: hh => T TC fsT. have Tc: sub T (substrate r). apply: (@sub_trans (comp C)) => //; apply: sub_setC. have Tf: inc T (free_subsets r) by apply/free_subsetsP. move: (gensiz _ Tf); case: (equal_or_not (cardinal T) (csucc k)); last first. move=> pa pb; apply /cltSleP => //; split => //. move => cTk _. pose Ci i := C +s1 i. pose Cip i F := finite_set F /\ sub F (substrate r) /\ forall X, sra F X -> forall Y, inc Y X -> ~ ( sub ((Ci i) \cap F) Y). have Cip1: forall i, inc i T -> exists F, Cip i F. move=> i iT; case: (p_or_not_p (gle sso C (Ci i))) => h. move: (TC _ iT) => /setC_P [_]; rewrite - (Cm _ h); case; apply: setU1_1. ex_middle ef; case: h. have cc: sub C (Ci i) by apply: sub_setU1. have cc2: sub (Ci i) (substrate r) by apply: setU1_sub => //; apply: Tc. apply /sub_gleP;split=> //;apply/ Zo_P; split;first by apply /setP_P. split => // F Fsf Fsr; ex_middle exp. case: ef; exists F;rewrite /Cip;split => //; split => // X p1 Y YX. case: (p_or_not_p (sub ((Ci i) \cap F) Y)) => //. move => bad2; case: exp; exists X => //; ex_tac. pose Ciq i := choose (fun F => Cip i F). have Cip2: forall i, inc i T -> Cip i (Ciq i). by move => i iT; apply: choose_pr; apply: Cip1. set G:= T \cup (unionb (Lg T Ciq)). have fG: finite_set G. apply: finite_union2; first by rewrite /finite_set cTk ; apply /NatP; fprops. apply: finite_union_finite; fprops; hnf; aw. by move=> i iT; rewrite LgV//; move: (Cip2 _ iT) => [Ok _]. hnf; rewrite cTk; apply /NatP; fprops. have Gs: sub G (substrate r). rewrite /G=> t; case /setU2_P; first by apply: Tc. move /setUb_P;aw; move=> [y yd]; rewrite LgV// => tC. by move: (Cip2 _ yd) => [_ [Ok _]]; apply: Ok. move: (cp2 _ fG Gs) => [X [cX [uX mdX] toX] [Y YX si]]. pose mp i := fun_image X (fun k => (Ciq i) \cap k). have Cip3: forall i, inc i T -> sra (Ciq i) (mp i). move=> i iT. have pr1:cardinal (mp i) <=c csucc k. set fa:= Lf (fun k => (Ciq i) \cap k) X (mp i). have ff: function fa. apply: lf_function; move=> t tX; apply /funI_P; ex_tac. move: (image_smaller ff). rewrite /fa; aw; set y := Imf _. have ->: y = (mp i). rewrite /y /mp/Imf lf_source. set Ta := [eta intersection2 (Ciq i)]. have aa: sub X (source (Lf Ta X (fun_image X Ta))) by aw. have bb: lf_axiom Ta X (fun_image X Ta) by move=> t tx; apply /funI_P; ex_tac. set_extens t. move /(Vf_image_P ff aa) => [z pa pb]; apply /funI_P; ex_tac. rewrite pb /fa LfV//. move /funI_P => [z pa pb] ;apply /(Vf_image_P ff aa); ex_tac. rewrite pb /fa LfV//. move=> le1; exact:(cleT le1 cX). have pr2: union (mp i) = Ciq i. set_extens t. move=> /setU_P [y ty] /funI_P [z zX izy]. by apply:(@setI2_1 _ z); rewrite - izy. move=> ti; apply /setU_P. have: inc t G. apply /setU2_P; right; apply /setUb_P; aw; exists i => //;rewrite LgV//. rewrite -uX => /setU_P [y ty yX]. exists ((Ciq i) \cap y) => //; first by apply /setI2_P. apply /funI_P; ex_tac. have pr3:disjoint_set (mp i). move=> a b /funI_P [za zaX ->] /funI_P [zb zbX ->]. case: (mdX _ _ zaX zbX); first by move=> ->; left. rewrite {1}/disjoint; right; apply: disjoint_pr => u. by move=> /setI2_P [_ ua] /setI2_P [_ ub]; empty_tac1 u; apply: setI2_i. split => // Y1 /funI_P [z zX ->]. have aux1: sub ((Ciq i) \cap z) z by apply: subsetI2r. exact:(sub_total_suborders2 or (toX _ zX) aux1). have TYe: T \cap Y = emptyset. apply /set0_P => y /setI2_P [yT yY]. move: (Cip2 _ yT) => [pa [pb pc]]; move: (pc _ (Cip3 _ yT)) => aux. have YMP: inc ((Ciq y) \cap Y) (mp y) by apply /funI_P; ex_tac. case: (aux _ YMP) => t /setI2_P [ta tb]; apply /setI2_P;split => //. move: ta; case /setU1_P; last move=> ->; fprops. move=> tC;apply: si; apply /setI2_P;split => //; apply /setU2_P;right. apply /setUb_P; aw; ex_tac; rewrite LgV//. have stu: sub T (union X) by rewrite uX /G; apply: subsetU2l. set k1:= cardinal X. have ksb: natp (csucc k) by fprops. have k1N: natp k1 by apply: (NS_le_nat cX ksb). move:cX; rewrite - cTk =>/eq_subset_cardP1/set_leP [T1 T1S]. move/card_eqP/esym; rewrite -/k1 => pa. have sm:(forall Z : Set, inc Z X -> small_set (T1 \cap Z)). move=> Z ZY x y /setI2_P [xT xZ] /setI2_P [yT yZ]. move: (T1S _ xT) (T1S _ yT) => xt1 yt1. have Zr': sub Z G by rewrite -uX; apply: setU_s1. move/total_subordersP: (toX _ ZY) => [Zr [orZ]]; rewrite iorder_sr// => tor. case: (tor _ _ xZ yZ)=> aux. by move: (iorder_gle1 aux); apply: fsT. by symmetry; move: (iorder_gle1 aux); apply: fsT. move: ((@Exercise4_5a X T1 k1 (refl_equal (cardinal X)) pa k1N (sub_trans T1S stu) mdX sm) _ YX). move=> [x]; aw => sx; move: (set1_1 x); rewrite - sx. move=> /setI2_P [ha hb]; empty_tac1 x; aw; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)