proposition: Lemma Dilworth_dual r (k := the_order_length r): order r -> (exists2 n, natp n & forall x, inc x (total_suborders r) -> cardinal x <=c n) -> exists A, [/\ natp k, order_length r k & [/\ partition_s A (substrate r), cardinal A = k & sub A (free_subsets r)]].
proof: Proof. move => or ha. have [res1 kN]: order_length r k /\ natp k. move: ha =>[n nN np]. apply: (the_max_card_on_set_prop nN (nonempty_total_suborders r) np). clear ha. move: (res1) => [[C Cto ca] cb]. set Cs := (total_suborders r). pose p x X:= [/\ inc X Cs, inc x X & forall y, inc y X -> gle r y x]. pose P x := Zo Cs (p x). pose f x := the_max_card_on_set (P x). have Ha x: inc x (substrate r) -> inc (singleton x) (P x). move => xsr. move: (set1_1 x) => xx. move: (torder_set1 or xsr) => hb. by apply: (Zo_i hb); split => // y /set1_P ->; order_tac. have bdP x X: inc X (P x) -> cardinal X <=c k. by move => /Zo_S; apply:cb. have Hx x: inc x (substrate r) -> max_card_on_set (P x) (f x) /\ natp (f x). move => xsr. have neP: nonempty (P x) by exists (singleton x); apply: Ha. apply: (the_max_card_on_set_prop kN neP (bdP x)). have fbd x: inc x (substrate r) -> \1c <=c (f x) /\ f x <=c k. move => xsr; move: (Hx x xsr) => [[qa qb] qc]; split. by move: (qb _ (Ha x xsr)); rewrite cardinal_set1. by move: qa => [X] /Zo_S /cb le <-. case: (emptyset_dichot (substrate r)) => Enz. exists emptyset; split => //. move:Cto =>/Zo_P [/setP_P /sub_smaller]; rewrite Enz cardinal_set0 ca. move => /cle0 -> _; split => //;last by move => t/in_set0. by split;[hnf; rewrite setU_0; split => // u v /in_set0| move => t /in_set0]. case: (equal_or_not k \0c) => knz. case: Enz => x /fbd [ua ub]; move: (cleT ua ub) => /cleNgt; case; ue. have finc x y: glt r x y -> f x <c f y. move => [lxy nxy]; move: (arg1_sr lxy) (arg2_sr lxy) => xsr ysr. move: (Hx _ xsr) => [[[c /Zo_P[/Zo_P[/setP_P ra rb] [_ qb qc]] lc] _] fN]. set Y := c +s1 y. have Ysr: sub Y (substrate r) by move => t/setU1_P; case => h; fprops; ue. have bmax: forall t, inc t Y -> gle r t y. move => t /setU1_P; case => h ; first by move: (qc _ h) => rc; order_tac. by rewrite h; order_tac. have yY: inc y Y by apply: setU1_1. have tor: total_order (induced_order r Y). move: (iorder_osr or Ysr) => [oa ob]; split => //. rewrite ob => a b aY bY; case/setU1_P: (bY); last first. by move => ->; left; apply/(iorder_gle0P r aY yY); apply: bmax. move => bX; case/setU1_P: (aY); last first. by move ->; right; apply/(iorder_gle0P r bY yY); apply: bmax. move => aX; move: (proj2 rb a b); rewrite (iorder_sr or ra) => h. by case: (h aX bX) => /iorder_gle1 cp; [left | right]; apply/(iorder_gleP). have Ys: inc Y Cs by apply: Zo_i => //; apply/setP_P. have Yb: inc Y (P y) by apply:(Zo_i Ys); split => //. have bx: ~ inc y c by move => /qc h; case: nxy; order_tac. move: (proj2(proj1 (Hx _ ysr)) _ Yb). rewrite /Y (csucc_pr bx); rewrite lc. by move/(cleSltP fN). pose A i := Zo (substrate r) (fun z => f z = i). pose AA := fun_image (Nint1c k) A. have ra : partition_w AA (substrate r). split. set_extens t. by move/setU_P=> [u tu /funI_P [i _ uv]]; move: tu; rewrite uv => /Zo_S. move => tsr; move /(Nint1cPb kN): (fbd _ tsr)=> fi. apply/setU_P. by exists (A (f t)); [apply/Zo_P | apply:funI_i]. move => a b /funI_P[i ia ->] /funI_P[j ka ->]; mdi_tac bad => t. by move=> /Zo_P [_ fti] /Zo_P[_ ftj]; case: bad; rewrite - fti - ftj. have Hb x: inc x AA -> inc x (free_subsets r). move/funI_P => [i _ ->]; apply: Zo_i; first by apply/setP_P => t /Zo_S. move => a b /Zo_P [_ fa] /Zo_P[_ fb] leab. by ex_middle bad; case: (proj2(finc _ _ (conj leab bad))); rewrite fa fb. have Akne: nonempty (A k). suff: exists2 x, inc x (substrate r) & f x = k. by move=> [x xde fx]; exists x; apply: Zo_i. move: (Cto) =>/Zo_P [/setP_P qa qb]. have fsC: finite_set C by apply /NatP; ue. have neC:nonempty C by apply/cle1P; rewrite ca; apply: cge1; fprops. have sr: substrate (induced_order r C) = C by rewrite iorder_sr. move: (finite_set_torder_greatest qb); rewrite sr => h. move: (h fsC neC) => [x []]; rewrite sr => xc xm. have cp: inc C (P x). apply:(Zo_i Cto); split => // y yC. exact: (iorder_gle1 (xm y yC)). move: (qa x xc) => xsr; exists x => //; apply: cleA. exact: (proj2 (fbd _ xsr)). by move: (Hx x xsr) => [ [_] xp] _; move: (xp _ cp); rewrite ca. have neA i: inc i (Nint1c k) -> nonempty (A i). case/(Nint1cPb kN);move: i; apply:(Nat_induction4 NS1 kN Akne). move => i le1 le2 [u /Zo_P [usr fu]]. move: (Hx u usr)=> [[[c /Zo_hi [qa qb qc] cs] _] nv]. move:(NS_lt_nat le2 kN) => iN. set D := c -s1 u. have cD: cardinal D = i by rewrite /D - (cpred_pr5 qb) cs fu (cpred_pr2 iN). have neD: nonempty D by apply/cle1P; ue. have fsD: finite_set D by apply /NatP; ue. have Dc: sub D c by move => t /setC1_P []. have qf: inc D Cs by apply: (sub_total_suborders2 or qa Dc). move/total_subordersP: (qf)=> [Dsr qe]. move: (iorder_sr or Dsr)=> ssr. move: (finite_set_torder_greatest qe); rewrite ssr => h. move: (h fsD neD)=> [x []]; rewrite ssr => xD xms. have xms' y : inc y D -> gle r y x by move/xms => /iorder_gle1. move/setC1_P: (xD)=>[xc xny]. have qg: inc D (P x) by apply: (Zo_i qf). exists x. apply: (Zo_i (Dsr _ xD)); apply: cleA. by apply/(cltSleP iN);rewrite - fu; apply:finc; split=> //;apply: (qc _ xc). by move:(proj2 (proj1 (Hx x (Dsr _ xD))) _ qg); rewrite cD. exists AA; split => //;split => //. by split => // t /funI_P [i ii ->]; apply: neA. rewrite - (card_Nint1c kN). apply:cardinal_fun_image=> a b ai bi eqa. move: (neA _ ai) => [x xA]; move/Zo_P: (xA) => [_ <-]. by rewrite eqa in xA; move/Zo_P: (xA) => [_ <-]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)