proposition: Lemma Exercise4_5b r k: finite_set (substrate r) -> order r -> natp k -> order_width r k -> Exercise4_5_conc r k.
proof: Proof. move /NatP; set n := cardinal (substrate r). move: (refl_equal n); rewrite {2} /n. move: n; move=> n nc nN; move: n nN r k nc; apply: Nat_induction1. move=> n nN hrec r k csr or kN [[X Xf cX] h2]. case: (emptyset_dichot (substrate r)) => sre. move: Xf => /Zo_P []; rewrite /Exercise4_5_conc sre; move /setP_P => Xse _. exists emptyset => //;split. + split;last by move=> a /in_set0. by split => //; try split => //; [rewrite setU_0 |move=> a b /in_set0]. + by move/sub_set0: Xse => <-. + by move=> x /in_set0. have fse: finite_set (substrate r) by hnf;rewrite - csr; apply /NatP; fprops. move: (finite_set_minimal or fse sre) => [a [asr amin]]. move: (csucc_pr1 (substrate r) a). rewrite (setC1_K asr) - csr; set E':= _ -s1 _ => eq1. set r' := induced_order r E'. have sE': sub E' (substrate r) by apply: sub_setC. move: (iorder_osr or sE')=> [or' sr']. set p1:= (cardinal E'). have p1c: p1 = (cardinal (substrate r')) by ue. have p1N: natp p1 by apply: (NS_nsucc (CS_cardinal E')); ue. move: (cltS p1N); rewrite - eq1 => p1n. have fsE T: inc T (free_subsets r') -> inc T (free_subsets r). move=> /free_subsetsP [p3 p2]; apply/free_subsetsP; split. by apply: (sub_trans _ sE'); ue. move => x y xt yt lexy;apply: p2=> //. by apply /iorder_gle0P => //;rewrite - sr'; apply: p3. have h21 x: inc x (free_subsets r') -> (cardinal x) <=c k. by move/fsE; apply: h2. rewrite - sr' in sE'. case: (p_or_not_p (exists2 X', inc X' (free_subsets r') & cardinal X' = k)); last first. move=> ne. set X1 := X -s1 a. have X1f: inc X1 (free_subsets r'). move/free_subsetsP: Xf => [p3 p2]; apply/free_subsetsP; split. by rewrite sr' => t /setC1_P [/p3 tX ta]; apply /setC1_P. move=> u v => /setC1_P [uX _] /setC1_P [vX _] uv. by move: (iorder_gle1 uv);apply: p2. case: (inc_or_not a X) => aX; last first. by case: ne; exists X => //; rewrite - (setC1_eq aX). move: (csucc_pr1 X a); rewrite setC1_K // -/X1 cX. set k1:= (cardinal X1) => ks. have kN': natp k1 by apply: NS_nsucc; rewrite /k1; fprops; ue. have krec: order_width r' k1. split; first by exists X1. move=> x xsr'; move: (h21 _ xsr') => le1. have: (cardinal x) <c k by split => // xk; case: ne; ex_tac. by rewrite ks; move /(cltSleP kN'). move: (hrec p1 p1n _ _ p1c or' kN' krec) => [Y [[[uY adi] ane] cY altY]]. have nauy: ~(inc a (union Y)). by rewrite uY sr' /E'; move /setC1_P => [_]. have nsY: ~ inc (singleton a) Y. move=> say; case: nauy; apply: (@setU_i _ (singleton a)); fprops. move: (csucc_pr nsY); rewrite cY -ks => p3. set Y' := (Y +s1 (singleton a)). have pr1: union Y' = substrate r. set_extens t. move=> /setU_P [y ty];case /setU1_P => tY. apply: sE'; rewrite -uY; union_tac. by move: ty; rewrite tY; move /set1_P => ->. move=> tsr; case: (equal_or_not t a) => ta. rewrite /Y' - ta;apply /setU_P; exists (singleton t);fprops. have: inc t (substrate r') by rewrite sr'; apply /setC1_P; fprops. rewrite /Y' -uY => /setU_P [y ty uyY]; union_tac. have pr2: disjoint_set Y'. move => u v; case /setU1_P => us; case /setU1_P => vs. + by apply: adi. + right; rewrite vs; apply: disjoint_pr => t tu /set1_P ta. case: nauy; rewrite -ta; union_tac. + right; rewrite us; apply: disjoint_pr => t /set1_P ta tu. case: nauy; rewrite -ta; union_tac. + by left;rewrite us vs. have pr3: alls Y' nonempty. move=> u; case /setU1_P; [ by apply: ane| move=> ->; apply: set1_ne]. exists (Y +s1 (singleton a)); split => //. move => x; case /setU1_P => xy. move /total_subordersP: (altY _ xy) => [sx []];rewrite iorder_sr // => orx torx. have sx1: sub x (substrate r). by apply: (@sub_trans (substrate r')) => //; rewrite sr' //. apply /total_subordersP; split; first exact. move: (iorder_osr or sx1) => [pa pb]. split => //; rewrite pb=> y z yx zx; case: (torx _ _ yx zx) => le1. - by left; apply /iorder_gleP => //;move: (iorder_gle1(iorder_gle1 le1)). - by right; apply /iorder_gleP => //;move: (iorder_gle1(iorder_gle1 le1)). have xsr: sub x (substrate r) by rewrite xy; apply: set1_sub. move: (iorder_osr or xsr) => [pa pb]. apply/total_subordersP; split =>//;split => //; rewrite pb xy;move=> y z. by move =>/set1_P -> /set1_P ->; left; apply /iorder_gle0P; fprops; order_tac. move=> h22. have krec: order_width r' k by []. move: (hrec p1 p1n _ _ p1c or' kN krec)=> [Y [[[uY adi] ane] cY altY]]. pose f T := Zo T (fun z => gle r a z). case: (p_or_not_p (exists2 Z, inc Z Y & forall T, inc T (free_subsets (induced_order r (E' -s (f Z)))) -> (cardinal T) <c k)). move => [Z ZY hZ]. set E'':= (E' -s (f Z)). set r'':= induced_order r E''. have sEs: sub E'' (substrate r). apply: (@sub_trans E') => //; apply: sub_setC. move: (iorder_osr or sEs) => [or'' sr'']. set X1:= X \cap (E' -s (f Z)). have X1f: inc X1 (free_subsets r''). apply/free_subsetsP;split; first by rewrite sr'';apply: subsetI2r. move=> x y /setI2_P [xX _] /setI2_P [yX _] le1. move: Xf => /Zo_P [p3 p2]. exact: (p2 x y xX yX (iorder_gle1 le1)). move: (hZ _ X1f) => le1. have knz: k <> \0c by move=> kz; rewrite kz in le1; case: (clt0 le1). move: (cpred_pr kN knz); set k1 := cpred k; move => [k1N k1s]. have krec1: order_width r'' k1. split; last by move=> x xr; move: (hZ _ xr);rewrite k1s; move/(cltSleP k1N). move: Xf => /Zo_P [] /setP_P aa bb. have cXp: forall x, inc x (X -s X1) -> (inc x X /\ (x = a \/ (inc x Z /\ gle r a x))). move=> x /setC_P [xX] /setI2_P => x1. split => //; case: (equal_or_not x a) => xa;first by left. right; ex_middle aux; case: x1; split => //; apply /setC_P;split => //. by apply /setC1_P;split => //; apply: aa. by apply /Zo_P. have sc: small_set (X -s X1). move=> x y xc yc; move: (cXp _ xc) (cXp _ yc) => [xX ex] [yX ey]. case: ex => xp; case: ey => yp. + by rewrite xp yp. + by move: yp; rewrite -xp; move => [_ xy]; apply: bb. + by symmetry;move: xp; rewrite -yp; move => [_ xy]; apply: bb. + move: xp yp => [xz _] [yz _]. move /total_subordersP: (altY _ ZY) => [Zs [orz]]; rewrite iorder_sr// => aux. by case: (aux _ _ xz yz) => le2;[ | symmetry]; move: (iorder_gle1 (iorder_gle1 le2)) => le3; apply:bb. have X1c: sub X1 X by apply: subsetI2l. move: (cardinal_setC X1c); rewrite cX k1s. have cX1: cardinalp (cardinal X1) by fprops. case: (small_set_pr sc) => cp1. rewrite /cdiff cp1 cardinal_set0 csum0r //. move=> le2; case: (proj2 le1); ue. rewrite /cdiff; move: cp1; move=> [x] ->. rewrite cardinal_set1 - csucc_pr4 // => ssc. by exists X1 => //; apply: csucc_inj; fprops. set p2 := cardinal (E' -s (f Z)). have p2c: p2 = cardinal (substrate r'') by ue. have ee'': sub E'' E' by apply: sub_setC. move: (sub_smaller ee''); rewrite -/p1 -/p2 => p12. have p2n:= cle_ltT p12 p1n. move: (hrec p2 p2n _ _ p2c or'' k1N krec1) => [Y' [[[uY' adi'] ane'] cY' altY']]. set U1 := (f Z) +s1 a. have nauy: ~(inc a (union Y')). by rewrite uY' sr''; move /setC_P => [] /setC1_P [_]. have nsY: ~ inc U1 Y'. move=> say; case: nauy; apply: (@setU_i _ U1); rewrite /U1;fprops. move: (csucc_pr nsY); rewrite cY' -k1s => p3. have Zr': sub Z (substrate r') by rewrite -uY; apply: setU_s1. have Zr: sub Z (substrate r) by apply: (@sub_trans (substrate r')). have U1r: sub U1 (substrate r). move=> t;case /setU1_P ; last by move => ->. by move /Zo_P => [tz _]; apply: Zr. set Y'' := Y' +s1 U1. have pr1:union Y'' = substrate r. set_extens t. move=> /setU_P [y ty /setU1_P[]] tY. apply: sEs; rewrite - sr'' -uY'; union_tac. move: ty; rewrite tY;apply: U1r. move=> tsr; apply /setU_P;case: (equal_or_not t a) => ta. rewrite ta/Y'';exists U1 => //; rewrite /U1;fprops. have tE': inc t E' by apply /setC1_P; split. case: (inc_or_not t (f Z)) => tf. exists U1 => //; rewrite /Y''/U1;fprops. have : inc t E'' by apply /setC_P; split. rewrite - sr'' -uY'/Y'';move=> /setU_P [y ty yy]; exists y; fprops. have aux: forall u,inc u Y' -> disjoint u U1. move => u uy; rewrite /U1;apply: disjoint_pr => t tu /setU1_P ta. have : inc t (union Y') by union_tac. case: ta; last by move => ->; apply: nauy. by rewrite uY' sr'' => tf; move /setC_P => [_]; case. have pr2:disjoint_set Y''. move => u v;case /setU1_P => us; case /setU1_P => vs. + by apply: adi'. + by right; rewrite vs; apply: aux. + by right; apply /disjoint_S;rewrite us; apply: aux. + by left;rewrite us vs. have pr3: alls Y'' nonempty. move=> u; case /setU1_P; [ by apply: ane'| move=> ->; exists a]. rewrite /U1;fprops. exists Y''; split => //. move => x;case /setU1_P => xy. move /total_subordersP: (altY' _ xy) => [sx []]; rewrite iorder_sr// => orx torx. have sx1: sub x (substrate r). by apply: (@sub_trans (substrate r'')) => //; rewrite sr'';apply: sEs. move: (iorder_osr or sx1) => [pa pb]. apply/total_subordersP; split => //. split => //; rewrite pb=> y z yx zx; case: (torx _ _ yx zx) => le2. by left; apply /iorder_gleP => //; move: (iorder_gle1 (iorder_gle1 le2)). by right;apply /iorder_gleP => //; move: (iorder_gle1(iorder_gle1 le2)). rewrite xy; apply:(total_suborder_prop or U1r) => x1 y1 x1u y1u. move/total_subordersP: (altY _ ZY)=> [_ [_]]; rewrite iorder_sr//; move=> torz. move: x1u y1u; case /setU1_P=> x1p; case /setU1_P => y1p. + move: x1p y1p => /Zo_S a1 /Zo_S a2. by case:(torz _ _ a1 a2) => /iorder_gle1 /iorder_gle1 h; [left | right]. + by rewrite y1p; move: x1p => /Zo_hi; right. + by rewrite x1p; move: y1p => /Zo_hi; left. + by rewrite x1p y1p; left; order_tac. pose io Z := (induced_order r (E' -s (f Z))). move=> bad. have Zp1: forall Z, sub (E' -s (f Z)) (substrate r). move=> Z ;by apply: (@sub_trans E'); [ apply: sub_setC | ue]. have Zp2: forall Z, substrate (io Z) = E' -s (f Z). move => Z;rewrite /io iorder_sr//. have sfr: forall Z T, inc Z Y -> inc T (free_subsets (io Z)) -> inc T (free_subsets r). move=> Z T ZY /Zo_P [] /setP_P pa pb; apply /Zo_P. move: (Zp1 Z)(Zp2 Z) => pc pd; rewrite pd in pa. split; first by apply /setP_P;apply: (@sub_trans (E' -s (f Z))). by move=> x y xT yT xy; apply: pb => //; apply /iorder_gle0P => //; apply: pa. have good: forall Z, inc Z Y -> exists2 T, inc T (free_subsets (io Z)) & cardinal T = k. move => Z ZY; ex_middle bad2. case: bad; exists Z => // T Tf. move: (sfr _ _ ZY Tf) => f1. split; first by apply: (h2 _ f1). case: (equal_or_not (cardinal T) k) => // Tk; case: bad2; ex_tac. pose g Z := choose(fun T => inc T (free_subsets(io Z)) /\ cardinal T = k). have gp1: forall Z, inc Z Y -> (inc (g Z) (free_subsets (io Z)) /\ cardinal (g Z) = k). by move=> Z /good [t ta tb]; apply choose_pr; exists t. clear bad good. pose krec1 T:= [/\ inc T (free_subsets r), sub T E' & cardinal T = k]. have gp2: forall Z, inc Z Y -> krec1 (g Z). move=> Z ZY; move: (gp1 _ ZY) => [pa pb]; split => //. apply: (sfr _ _ ZY pa). move: pa =>/Zo_P [] /setP_P pa _. apply: (sub_trans pa); rewrite /io iorder_sr //; apply: sub_setC. have gp3: forall T Z, krec1 T -> inc Z Y -> small_set (T \cap Z). move=> T Z [pa pb pc] ZY x y /setI2_P [xT xZ] /setI2_P [yT yZ]. move: pa => /Zo_P [_ aux2]. move /total_subordersP: (altY _ ZY) => [Zr'[_]]; rewrite iorder_sr//;move=> tor. have Zr: sub Z (substrate r) by apply: (@sub_trans (substrate r')). case: (tor _ _ xZ yZ)=> aux. by move: (iorder_gle1 (iorder_gle1 aux)); apply: aux2. by symmetry; move: (iorder_gle1 (iorder_gle1 aux)); apply: aux2. have gp4: forall T Z, krec1 T -> inc Z Y -> singletonp (T \cap Z). move => T Z kr; move: (kr) => [kt1 kt2 kt3]. have stu: sub T (union Y) by rewrite uY sr'. apply: (Exercise4_5a cY kt3 kN stu adi). move=> z zy;apply: (gp3 _ _ kr zy). pose sij z1 z2 := union ((g z1) \cap z2). have sijp: forall z1 z2, inc z1 Y -> inc z2 Y -> (g z1) \cap z2 = singleton (sij z1 z2). move=> z1 z2 z1Y z2Y; rewrite /sij; move: (gp4 _ _ (gp2 _ z1Y) z2Y) => [s] ->. by rewrite setU_1. have sij1: forall i j, inc i Y -> inc j Y -> inc (sij i j) (g i). move => i j iY jY; apply: (@setI2_1 _ j). rewrite (sijp _ _ iY jY); fprops. have sij2: forall i j, inc i Y -> inc j Y -> inc (sij i j) j. move => i j iY jY; apply: (@setI2_2 (g i)). rewrite (sijp _ _ iY jY); fprops. have sija1: forall i j, inc i Y -> inc j Y -> gle r (sij i j) a-> False. move=> i j iY jY; move: (sij1 _ _ iY jY) => aux2. move: (gp1 _ iY) => [] /Zo_P [] /setP_P; rewrite /io iorder_sr // => s1 _. move: (s1 _ aux2) => /setC_P [] /Zo_P [pa] /set1_P pb pc _. by move => aux1; move: (amin _ aux1). have sija2: forall i, inc i Y-> gle r a (sij i i) -> False. move=> i iY; move: (sij1 _ _ iY iY) => pa pc. move: (gp1 _ iY) => [] /Zo_P [] /setP_P; rewrite /io iorder_sr // => s1 _. move: (s1 _ pa) => /setC_P [] /Zo_P [pb] /set1_P pe pd _. by case: pd; apply: Zo_i=> //; apply: sij2. pose V1 j:= fun_image Y (fun i => sij i j). pose sj j := the_least (induced_order r (V1 j)). have v1p: forall j, inc j Y -> let r1 := (induced_order r (V1 j)) in [/\ order r1, substrate r1 = V1 j & least r1 (sj j)]. move=> j jY r1. have s1: sub (V1 j) j. move => t /funI_P [z zY ->]; apply: (sij2 _ _ zY jY). have s0: sub j (substrate r') by move=> t tj;rewrite -uY; union_tac. have s2:= (sub_trans s1 s0). have s3:= (sub_trans s2 sE'). have s4:= (sub_trans s0 sE'). move: (iorder_osr or s3) => [or1 pb]. have ne1: nonempty (V1 j) by exists (sij j j); apply /funI_P; ex_tac. have fs1: finite_set (V1 j) by apply: ( sub_finite_set s3 fse). rewrite /r1;saw; apply: the_least_pr => //. have s5: sub (V1 j) (substrate (induced_order r j)) by rewrite iorder_sr. move/total_subordersP:(altY _ jY) => [_ tor1]. rewrite - (iorder_trans r s1). apply: finite_subset_torder_least => //. rewrite - (iorder_trans r s0) sr'//. have v2p: forall i j, inc i Y -> inc j Y -> gle r (sj i) (sj j) -> i = j. move=> i j iY jY leij. move: (v1p _ iY) (v1p _ jY) => [o1 sr1 le1][o2 sr2 le2]. move: le1 => []; rewrite sr1; move /funI_P => [z zY sa] _. have sb: inc (sij z j) (substrate (induced_order r (V1 j))). rewrite sr2; apply /funI_P; ex_tac. move:le2 => [le3 le4]; move: (le4 _ sb) => le5. move: (order_transitivity or leij (iorder_gle1 le5)); rewrite sa => le6. move: (sijp _ _ zY iY)(sijp _ _ zY jY) => s1 s2. move: (gp2 _ zY) => [fk _]; move: fk => /Zo_P [_ fk2]. move: (fk2 _ _ (sij1 _ _ zY iY) (sij1 _ _ zY jY) le6). move: (sij2 _ _ zY iY) (sij2 _ _ zY jY) => i1 i2 sv. case: (adi _ _ iY jY) => //; rewrite /disjoint => di. empty_tac1 (sij z i); apply: setI2_i => //; ue. set V2 := fun_image Y sj. have sii: forall j, inc j Y-> exists2 i, inc i Y & sj j = sij i j. move=> j jY; move: (v1p _ jY) => [pa pb [pc pd]]. move:pc; rewrite pb => /funI_P [z zY ->]; ex_tac. have v3p: forall j, inc j Y -> inc (sj j) (substrate r). move=> l lY;move: (sii _ lY) => [j jY ->]. apply: sE'; rewrite -uY; move: (sij2 _ _ jY lY) => su; union_tac. have c2: cardinal V2 = k. symmetry; rewrite - cY; apply /card_eqP. exists (Lf sj Y V2); hnf; rewrite lf_source lf_target; split => //. apply: lf_bijective. move=> t TY; apply /funI_P; ex_tac. move=> u v uY1 vY ss; apply: (v2p _ _ uY1 vY); rewrite - ss; order_tac. by apply: v3p. by move => y /funI_P. set v3:= V2 +s1 a. have an2: ~ (inc a V2). move=> /funI_P [z zY]; move: (sii _ zY) => [j jY] -> ta. by case: (sija1 _ _ jY zY); rewrite - ta; order_tac. move: (csucc_pr an2); rewrite c2;set (V3:= V2 +s1 a) => bad1. have V3t: inc V3 (free_subsets r). apply: Zo_i. apply /setP_P => t; case /setU1_P; last by move => ->. by move=> /funI_P [z zY ->];apply: v3p. move=> x y ; case /setU1_P => pa; case /setU1_P => pb. + move: pa pb => /funI_P [z zY ->] /funI_P [z' zY' ->]. by move=> aux; rewrite (v2p _ _ zY zY' aux). + rewrite pb; move: pa => /funI_P [z zY ->]. move: (sii _ zY) => [j jY ->] le1. case: (sija1 _ _ jY zY le1). + rewrite pa; move: pb => /funI_P [z zY ->]. move: (v1p _ zY) => [qa qb [qc qd]] asj; rewrite qb in qd. have sb: inc (sij z z) (V1 z) by apply /funI_P; ex_tac. move: (order_transitivity or asj (iorder_gle1 (qd _ sb))) => le2. case: (sija2 _ zY le2). + by rewrite pa pb. move: (h2 _ V3t); rewrite bad1 => pa; case: (cleNgt pa (cltS kN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)