proposition: Lemma order_length_exists r (k := the_order_length r): finite_set (substrate r) -> [/\ natp k, k <=c (cardinal (substrate r)) & order_length r k].
proof: Proof. move => /NatP nN. have sf x:inc x (total_suborders r) -> cardinal x <=c cardinal (substrate r). by move => /Zo_S /setP_P/sub_smaller. have nef:= nonempty_total_suborders r. move: (the_max_card_on_set_prop nN nef sf) =>[ra rb]; split => //. by move: (proj1 ra) => [x/sf ccx eq]; rewrite eq in ccx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)