proposition: Lemma Exercise4_5b_alt 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]. have fsr: finite_set(substrate r) by apply/NatP; ue. move: (order_length_exists fsr); set ol:= the_order_length _. move => [olN oln [[C /total_subordersP [Csr Ctot]cC] olb]]. have dots u v: gle r u v -> inc (doubleton u v) (total_suborders r). move=> luv; move: (arg1_sr luv) (arg2_sr luv) => usr vsr. set Y := doubleton u v. have sY: sub Y (substrate r) by apply: sub_set2. apply:(total_suborder_prop or sY) => a b /set2_P [] -> /set2_P [] ->. - by left; order_tac. - by left. - by right. - by right; order_tac. case: (NleT_el NS2 olN) => ol2; last first. move: (greatest_is_partition (substrate r)). set A := greatest_partition _ => h. have cA: cardinal A = cardinal (substrate r). by apply: (cardinal_fun_image) => i j _ _; apply:set1_inj. have At: sub A (total_suborders r). move => t /funI_P[z zsr ->]; apply:(total_suborder_prop or (set1_sub zsr)). by move => a b /set1_P -> /set1_P ->; left; order_tac. have /h2 le1: inc (substrate r) (free_subsets r). apply/free_subsetsP; split => // u v usr vsr luv; ex_middle bad. move: (dots _ _ luv). by move/olb; rewrite (cardinal_set2 bad) => /cleNgt; case. exists A; split => //; rewrite cA; apply: cleA => //. by move/free_subsetsP: Xf => [/sub_smaller]; rewrite cX. move: (iorder_osr or Csr) => [orC sioC]. have fsC: finite_set (substrate (induced_order r C)). by rewrite sioC; apply /NatP; ue. have neC: nonempty (substrate (induced_order r C)). rewrite sioC; apply /cle1P; rewrite cC; exact: (cleT cle_12 ol2). move: (finite_set_torder_least Ctot fsC neC) =>[alpha []]. move: (finite_set_torder_greatest Ctot fsC neC) => [omga []]. rewrite sioC => oC oop aC aap. have olC x: inc x C -> gle r x omga by move/oop/ iorder_gle1. have alC x: inc x C -> gle r alpha x by move/aap/ iorder_gle1. move:(alC _ oC) => lab. case: (equal_or_not alpha omga) => nab. have cv : C = singleton alpha . apply :set1_pr => // x xC; move: (olC _ xC) (alC _ xC); rewrite - nab. move => qa qb; order_tac. move: (cardinal_set1 alpha); rewrite - cv cC=> ea. case: (cleNgt ol2); rewrite ea; exact: (clt_12). have ltab: glt r alpha omga by split. move: (arg1_sr lab) (arg2_sr lab) => aE oE. clear oop aap lab nab. pose E' := (substrate r) -s (doubleton alpha omga). have sub1: sub E' (substrate r) by move => t /setC_P []. move: (iorder_osr or sub1); set r1:= induced_order _ _; move =>[or1 sr1]. have fs1: finite_set (substrate r1). by rewrite sr1; apply: (sub_finite_set sub1 fsr). move: (order_width_exists fs1); set k1 := the_order_width _. move => [k1N kbd owrk1]; move: (owrk1) => [[X1 cX1 x1p] k1max]. move/free_subsetsP: cX1 => [X1sr X1free]. have Xfree a b: inc a X1 -> inc b X1 -> gle r a b -> a = b. move => ax bx le; apply:(X1free a b ax bx);apply/iorder_gleP. by split => //; rewrite - sr1; apply: X1sr. have le1: k1 <=c k. suff: inc X1 (free_subsets r) by move/ h2; rewrite x1p. apply/free_subsetsP. split; first by apply: (sub_trans X1sr); rewrite sr1. by move => u v ux1 vx1 le1; apply:(Xfree u v ux1 vx1). have: k = k1 \/ k = csucc k1. set X2 := X \cap E'. have sr2: sub X2 (substrate r1) by rewrite sr1 => t /setI2_P []. move/free_subsetsP: Xf => [qa qb]. have: inc X2 (free_subsets r1). apply/free_subsetsP; split => // u v /setI2_P [uX _] /setI2_P[vX _]. by move/iorder_gle1; apply:qb. move/k1max => le2. have aux: cardinal X = csucc (cardinal X2) -> k = k1 \/ k = csucc k1. move => h. case: (equal_or_not k1 k) =>kk1; [ by left | right]. have: k1 <c k by split. by move/(cleSltP k1N); apply: cleA; move: (cleSS le2); rewrite - cX - h. case: (inc_or_not alpha X)=> hb; case: (inc_or_not omga X) => ha. - case: (proj2 ltab); exact: (qb _ _ hb ha (proj1 ltab)). - apply: aux. have ->: X = X2 +s1 alpha. set_extens t; last by case/setU1_P; [ case/setI2_P | move ->]. move => tx; apply/setU1_P; case: (equal_or_not t alpha). by move ->; right. move => ta; left; apply/setI2_P; split => //; apply/setC_P; split. by apply: qa. case /set2_P => // to; case: ha; ue. rewrite csucc_pr //; case/setI2_P => _ /setC_P [_]; case; fprops. - apply: aux. have ->: X = X2 +s1 omga. set_extens t; last by case/setU1_P; [ case/setI2_P | move ->]. move => tx; apply/setU1_P; case: (equal_or_not t omga). by move ->; right. move => ta; left; apply/setI2_P; split => //; apply/setC_P; split. by apply: qa. case /set2_P => // to; case: hb; ue. rewrite csucc_pr //; case/setI2_P => _ /setC_P [_]; case; fprops. - left; apply: cleA => //; move: le2; rewrite - cX. have -> //: X2 = X. set_extens t; [ by move/setI2_P => [] | move => tx; apply/setI2_P]. split => //; apply/setC_P; split; try apply: qa => //. case/set2_P => tv; [ case: hb; ue | case: ha; ue ]. case => kk1; last first. have cE: cardinal E' <c n. apply/(cleSlt0P (CS_cardinal _) nN); rewrite csr (csucc_pr2 aE). have /sub_smaller /cleSS //: sub E' (substrate r -s1 alpha). move => t /setC_P [tr h]; apply/setC1_P; split => // ta; case: h; ue. have sdr: sub (doubleton alpha omga) (substrate r) by apply: sub_set2. have cE2: E' =c substrate r1 by rewrite - sr1. move: (hrec _ cE r1 k1 cE2 or1 k1N owrk1) => [x2 [[[pa pb] pc] x2b x2c]]. exists (x2 +s1 (doubleton alpha omga)); split => //. - split; first split. + set_extens t. move/setU_P => [y ty /setU1_P]; case => yp. apply: sub1; rewrite - sr1 - pa; union_tac. by move: ty; rewrite yp; apply: sdr. move => tsr; case: (inc_or_not t (doubleton alpha omga)) => td. apply/setU_P; exists (doubleton alpha omga); fprops. have : inc t E' by apply/setC_P. rewrite - sr1 -pa => /setU_P [y ya yb]; union_tac. + move => a b aU bU; case/setU1_P: aU; case/setU1_P: bU => bu au. * exact: (pb a b au bu). * mdi_tac h => x xa; rewrite bu. have /setC_P [_ xd] //: inc x E' by rewrite - sr1 - pa; union_tac. * mdi_tac h => x; rewrite au => xd xb. have /setC_P [_] //: inc x E' by rewrite - sr1 - pa; union_tac. * by rewrite au bu; left. + move => t /setU1_P; case; [ by apply: pc | move ->; apply:set2_ne]. - rewrite csucc_pr ? x2b // => dx2. have /setC_P [_ /set2_P]: inc alpha E' by rewrite - sr1 - pa; union_tac. by case; left. - move => t/setU1_P []; first by move/x2c; apply:sub_total_suborders1. move ->; apply: (dots _ _ (proj1 ltab)). pose Ep := Zo (substrate r) (fun z => exists2 a, inc a X1 & gle r a z). pose Em := Zo (substrate r) (fun z => exists2 a, inc a X1 & gle r z a). have Epmu: Ep \cup Em = substrate r. set_extens t; first by case/setU2_P => /Zo_S. move => tsr; apply/setU2_P; case: (inc_or_not t X1) => tx1. by left; apply: (Zo_i tsr); ex_tac; order_tac. have qc: sub X1 E' by ue. case: (p_or_not_p (forall a, inc a X1 -> ~ (gle r a t))) => hA; last first. left; apply: (Zo_i tsr); ex_middle bad; case: hA => a aX1 ba. case: bad; ex_tac. case: (p_or_not_p (forall a, inc a X1 -> ~ (gle r t a))) => hB; last first. right; apply: (Zo_i tsr); ex_middle bad; case: hB => a aX1 ba. case: bad; ex_tac. have: inc (X1 +s1 t) (free_subsets r). apply/free_subsetsP; split; first by apply: setU1_sub => // w /qc /sub1. move => a b /setU1_P aa /setU1_P bb l21; case: aa;case:bb=> aa bb. + by apply: Xfree. + by case: (hA _ bb); rewrite - aa. + by case: (hB _ aa); rewrite - bb. + by rewrite aa bb. by move/h2; rewrite csucc_pr // x1p - kk1 => /cleNgt; case; apply/cltS. have Epmi : Ep \cap Em = X1. set_extens t. move=> /setI2_P [ /Zo_P [tsr [a aX1 le2]] /Zo_P [_ [b bX1 le3]]]. move: (Xfree a b aX1 bX1 (proj43 or _ _ _ le2 le3)) => eab. have <- //: a = t by rewrite - eab in le3; order_tac. move => tx1; move: (X1sr _ tx1); rewrite sr1 => /sub1 tE. by apply/setI2_P; split; apply: (Zo_i tE); ex_tac; order_tac. have sX1Ep: sub X1 Ep by rewrite - Epmi => t /setI2_P []. have sX1Em: sub X1 Em by rewrite - Epmi => t /setI2_P []. case: (inc_or_not alpha Ep). move=> /Zo_P [ asr [a ax1 lear]]. case: (equal_or_not a alpha) => eaa. move:(X1sr _ ax1); rewrite eaa sr1 => /setC_P [_];case; fprops. have naC: ~ inc a C by move/alC => le2; case: eaa; order_tac. set C2 := C +s1 a. suff : inc C2 (total_suborders r). by move/ olb; rewrite (csucc_pr naC) cC => /cleNgt; case; apply/cltS. have C2sr: sub C2 (substrate r). move => t /setU1_P; case; [ apply: Csr | move ->; order_tac]. apply:(total_suborder_prop or C2sr) => u v /setU1_P [] uc /setU1_P [] vc. + move: (proj2 Ctot); rewrite sioC => h; case:(h _ _ uc vc) => /iorder_gle1. by move => le; left. by move => le; right. + rewrite vc; right; move: (alC _ uc) => le3; order_tac. + rewrite uc; left; move: (alC _ vc) => le3; order_tac. + rewrite uc vc; left; order_tac; order_tac. case: (inc_or_not omga Em). move=> /Zo_P [ asr [a ax1 lear]]. case: (equal_or_not a omga) => eaa. move:(X1sr _ ax1); rewrite eaa sr1 => /setC_P [_];case; fprops. have naC: ~ inc a C by move/olC => le2; case: eaa; order_tac. set C2 := C +s1 a. suff : inc C2 (total_suborders r). by move/ olb; rewrite (csucc_pr naC) cC => /cleNgt; case; apply/cltS. have C2sr: sub C2 (substrate r). move => t /setU1_P; case; [ apply: Csr | move ->; order_tac]. apply:(total_suborder_prop or C2sr) => u v /setU1_P [] uc /setU1_P [] vc. + move: (proj2 Ctot); rewrite sioC => h; case:(h _ _ uc vc) => /iorder_gle1. by move => le; left. by move => le; right. + rewrite vc; left; move: (olC _ uc) => le3; order_tac. + rewrite uc; right; move: (olC _ vc) => le3; order_tac. + rewrite uc vc; left; order_tac; order_tac. move => Ems Eps. have subp: sub Ep (substrate r) by apply:Zo_S. have subm: sub Em (substrate r) by apply:Zo_S. case:(iorder_osr or subp); case(iorder_osr or subm). set rm := induced_order _ _; set rp := induced_order _ _ => orm srm orp srp. have eqp: Ep =c substrate rp by ue. have eqm: Em =c substrate rm by ue. have ltp: cardinal Ep <c n. apply/(cleSlt0P (CS_cardinal _) nN);rewrite - (csucc_pr Eps) csr. by apply: sub_smaller; apply: setU1_sub. have ltm: cardinal Em <c n. apply/(cleSlt0P (CS_cardinal _) nN);rewrite - (csucc_pr Ems) csr. by apply: sub_smaller; apply: setU1_sub. clear Ems Eps. have wrpk: (order_width rp k). have ha: sub X1 (substrate rp) by rewrite srp. have fr1: inc X1(free_subsets rp). apply/free_subsetsP; split => //. by move => a b aX1 bX1 /iorder_gle1 le;apply: Xfree. split; first by ex_tac; rewrite x1p. move => T /free_subsetsP [qc qd]; apply: h2; apply/free_subsetsP. have Tsr: sub T (substrate r) by apply: (sub_trans qc); rewrite srp. rewrite srp in qc. split => //a b aT bT leab; apply: qd => //; apply/iorder_gleP; split; fprops. have wrmk: (order_width rm k). have ha: sub X1 (substrate rm) by rewrite srm. have fr1: inc X1(free_subsets rm). apply/free_subsetsP; split => //. by move => a b aX1 bX1 /iorder_gle1 le;apply: Xfree. split; first by ex_tac; rewrite x1p. move => T /free_subsetsP [qc qd]; apply: h2; apply/free_subsetsP. have Tsr: sub T (substrate r) by apply: (sub_trans qc); rewrite srm. rewrite srm in qc. split => //a b aT bT leab; apply: qd => //; apply/iorder_gleP; split; fprops. case: (hrec _ ltp _ _ eqp orp kN wrpk). case: (hrec _ ltm _ _ eqm orm kN wrmk). rewrite srm srp => Pm [Pma Pmb Pmc] Pp [Ppa Ppb Ppc]. pose FP x := select (fun z => inc x z). have HFP E P: partition_s P E -> forall x, inc x E -> inc x (FP x P) /\ inc (FP x P) P. move => [[qa qb] qc] x xE; apply: select_pr. rewrite - qa in xE; move /setU_P: xE=> [y ya yb]; ex_tac. move => a b /= aY xa bY xb; case: (qb a b aY bY) => // dab; empty_tac1 x. pose fp x:= select (fun z => inc x z) Pp. have Hap x: inc x Ep -> inc x (fp x) /\ inc (fp x) Pp by apply: HFP. pose fm x:= select (fun z => inc x z) Pm. have Ham x: inc x Em -> inc x (fm x) /\ inc (fm x) Pm by apply: HFP. have injfp: {inc X1 &, injective fp}. move => x y xX1 yX1 /=; move: (Hap _ (sX1Ep _ xX1)) (Hap _ (sX1Ep _ yX1)). move => [pa pb] [pc pd] pe; rewrite - pe in pc. move:(Ppc _ pb) => /total_subordersP [qa qb]. move: (proj2 qb x y); rewrite iorder_sr // => h; move: (h pa pc). case=>/iorder_gle1 /iorder_gle1 => le. by apply:(Xfree _ _ xX1 yX1). by symmetry;apply:(Xfree _ _ yX1 xX1). have injfm: {inc X1 &, injective fm}. move => x y xX1 yX1 /=; move: (Ham _ (sX1Em _ xX1)) (Ham _ (sX1Em _ yX1)). move => [pa pb] [pc pd] pe; rewrite - pe in pc. move:(Pmc _ pb) => /total_subordersP [qa qb]. move: (proj2 qb x y);rewrite iorder_sr // => h; move: (h pa pc). case=>/iorder_gle1 /iorder_gle1 => le. by apply:(Xfree _ _ xX1 yX1). by symmetry;apply:(Xfree _ _ yX1 xX1). have cX1: cardinal X1 = k by ue. have fsX1: finite_set X1 by apply /NatP; ue. have axp: lf_axiom fp X1 Pp by move => x /sX1Ep /Hap[]. have axm: lf_axiom fm X1 Pm by move => x /sX1Em /Ham[]. have bijfp: bijection (Lf fp X1 Pp). by apply:bijective_if_same_finite_c_inj; aw; trivial;try ue; apply: lf_injective. have bijfm: bijection (Lf fm X1 Pm). by apply:bijective_if_same_finite_c_inj; aw; trivial;try ue; apply: lf_injective. pose fpm x := fp x \cup fm x. have ra: union (fun_image X1 fpm) = substrate r. set_extens t. move/setU_P => [y ty /funI_P [z zx1 yv]]. move: ty; rewrite yv => /setU2_P []. move: (Hap _ (sX1Ep _ zx1)) => [za zb] tp; apply: subp. rewrite - (proj1 (proj1 Ppa)); union_tac. move: (Ham _ (sX1Em _ zx1)) => [za zb] tp; apply: subm. rewrite - (proj1 (proj1 Pma)); union_tac. rewrite - Epmu => /setU2_P; case. rewrite - (proj1 (proj1 Ppa)) => /setU_P [y ty yp]. move: (proj2 (proj2 bijfp) y); aw => h; move:(h yp) => [x xX1]; rewrite LfV// => yv. by apply/setU_P; exists (fpm x); [ apply/setU2_P; left; ue | apply:funI_i]. rewrite - (proj1 (proj1 Pma)) => /setU_P [y ty yp]. move: (proj2 (proj2 bijfm) y); aw => h; move:(h yp) => [x xX1]; rewrite LfV// => yv. by apply/setU_P; exists (fpm x); [ apply/setU2_P; right; ue | apply:funI_i]. have aux i j x: inc i X1 -> inc j X1 -> inc x (fp i) -> inc x (fm j)-> i= j. move => ix jx xxi xxj. move: (Hap _ (sX1Ep _ ix)) (Ham _ (sX1Em _ jx)) => [qa qb][qc qd]. move: Ppa Pma => [[sa sb] _] [[sc sd] _]. have xp: inc x Ep by rewrite - sa; union_tac. have xm: inc x Em by rewrite - sc; union_tac. have xx1: inc x X1 by rewrite - Epmi; fprops. have -> : i = x. move: (Ppc _ qb) => /total_subordersP [qe [qf]]. rewrite (iorder_sr orp qe) => tt; move: (tt i x qa xxi). case; move/iorder_gle1/iorder_gle1=> cp. exact:(Xfree i x ix xx1 cp). by rewrite (Xfree x i xx1 ix cp). have -> // : j = x. move: (Pmc _ qd) => /total_subordersP [qe [qf]]. rewrite (iorder_sr orm qe) => tt; move: (tt j x qc xxj). case; move/iorder_gle1/iorder_gle1=> cp. exact:(Xfree j x jx xx1 cp). by rewrite (Xfree x j xx1 jx cp). have aux2 x i j: inc i X1 -> inc j X1 ->inc x (fpm i) -> inc x (fpm j) -> i = j. move: Ppa Pma => [[sa sb] _] [[sc sd] _] ix jx. case/setU2_P => xx; case/setU2_P => yy. + move: (Hap _ (sX1Ep _ ix)) (Hap _ (sX1Ep _ jx)) => [qa qb][qc qd]. move: (sb _ _ qb qd); case => sf; last by empty_tac1 x. by move:(injfp _ _ ix jx sf) => ->. + by rewrite (aux _ _ _ ix jx xx yy). + by rewrite (aux _ _ _ jx ix yy xx). + move: (Ham _ (sX1Em _ ix)) (Ham _ (sX1Em _ jx)) => [qa qb][qc qd]. move: (sd _ _ qb qd); case => sf; last by empty_tac1 x. by rewrite(injfm _ _ ix jx sf). have rb: partition_s (fun_image X1 fpm) (substrate r). split; first split => //. move => a b /funI_P[i ix ->] /funI_P[j jx ->]; mdi_tac hh => x x1 x2. by case: hh; rewrite (aux2 x i j ix jx x1 x2). move => t /funI_P [z zX1 ->]; move: (proj1(Hap _ (sX1Ep _ zX1))) => zi. by exists z; apply/setU2_P; left. have rc: cardinal (fun_image X1 fpm) = k. rewrite cardinal_fun_image // => i j ix jx hh. move: (proj1 (Hap _ (sX1Ep _ ix))) => qa. have qb: inc i (fpm i) by apply/setU2_P; left. have qc: inc i (fpm j) by ue. exact:(aux2 i i j ix jx qb qc). exists (fun_image X1 fpm); split => // t /funI_P [x x1 ->]. move: (Hap _ (sX1Ep _ x1)) (Ham _ (sX1Em _ x1)) => [qa qb][qc qd]. move: Ppa Pma => [[sa sb] _] [[sc sd] _]. have s1: sub (fpm x) (substrate r). move => y /setU2_P [] yy; first by apply: subp; rewrite - sa; union_tac. apply: subm; rewrite - sc; union_tac. have hp a b: inc a (fp x) -> inc b (fp x) -> ocomparable r a b. move/total_subordersP: (Ppc _ qb) => [pa [pb]]. rewrite (iorder_sr orp pa) => hp af bf. by case: (hp a b af bf) => /iorder_gle1/iorder_gle1; [left | right]. have hm a b: inc a (fm x) -> inc b (fm x) -> ocomparable r a b. move/total_subordersP: (Pmc _ qd) => [pa [pb]]. rewrite (iorder_sr orm pa) => hm af bf. by case: (hm a b af bf) => /iorder_gle1/iorder_gle1; [left | right]. have hap a: inc a (fp x) -> gle r x a. move => afp. have: inc a Ep by rewrite - sa; union_tac. move=> /Zo_P [asr [b bX1 le2]]; case:(hp x a qa afp) => // lax. by rewrite - (Xfree _ _ bX1 x1 (proj43 or _ _ _ le2 lax)). have ham a: inc a (fm x) -> gle r a x. move => afp. have: inc a Em by rewrite - sc; union_tac. move=> /Zo_P [asr [b bX1 le2]]; case:(hm x a qc afp) => // lax. by rewrite (Xfree _ _ x1 bX1 (proj43 or _ _ _ lax le2)). apply:(total_suborder_prop or s1) => a b;case/setU2_P => xx; case/setU2_P => yy. + by apply: hp. + right; move: (hap _ xx) (ham _ yy) => la lb; order_tac. + left; move: (ham _ xx) (hap _ yy) => la lb; order_tac. + by apply: hm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)