proposition: Lemma Dilworth_lemma_v2 r n m: order r -> natp n -> natp m -> cardinal (substrate r) = csucc (n *c m) -> (exists2 B, inc B (free_subsets r) & cardinal B = csucc m) \/ exists2 A, inc A (total_suborders r) & cardinal A = csucc n.
proof: Proof. move => or nN mN csr. move: (NS_succ (NS_prod nN mN)); set p := csucc _ => pN. have fsr: finite_set (substrate r) by apply/NatP; ue. move:(Dilworth_lemma_v1 or fsr). move: (order_length_exists fsr) (order_width_exists fsr). set a := (the_order_length r); set b := (the_order_width r); rewrite csr. move => [aN ab [ [A Af cA] _]] [bN bb [ [F Ff cF] _]] le1. case: (NleT_el aN nN) => le2. case: (NleT_el bN mN) => le3. case: (cleNgt(cleT le1 (cprod_Mlele le2 le3))); apply: cltS; fprops. left; move/(cleSltP mN): le3; rewrite -(card_card (CS_succ m)) - cF. move/ (sub_smaller_contra) => [Y yf ->]; exists Y => //. move/free_subsetsP:Ff => [ra rb]. apply/free_subsetsP; split; first by apply: (sub_trans yf ra). by move => u v /yf ua /yf ub; apply: rb. right; move/(cleSltP nN): le2; rewrite -(card_card (CS_succ n)) - cA. move/ (sub_smaller_contra) => [Y yf ->]; exists Y => //. exact:(sub_total_suborders2 or Af yf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)