proposition: Lemma Dilworth_lemma_v1 r : order r -> finite_set (substrate r) -> cardinal (substrate r) <=c (the_order_length r) *c (the_order_width r).
proof: Proof. move => or fsr. move: (order_length_exists fsr) (order_width_exists fsr). set k := the_order_width r; set l := the_order_length r. move => [lN lb [qa qb]] [kN kb [qc qd]]. have hll: (exists2 n, natp n & forall x, inc x (total_suborders r) -> cardinal x <=c n) by exists l. move:(Dilworth_dual or hll); rewrite -/l. move => [A [_ _ [pa pb pc]]]. rewrite - (proj1 (proj1 pa)) - pb cprodC. by apply: cardinal_uniona => x /pc /qd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)