proposition: Lemma order_width_exists r (k := the_order_width r): finite_set (substrate r) -> [/\ natp k, k <=c (cardinal (substrate r)) & order_width r k].
proof: Proof. move => /NatP nN. have nef:= nonempty_free_subsets r. have sf x: inc x (free_subsets r) -> cardinal x <=c (cardinal (substrate r)). by move => /Zo_S /setP_P/sub_smaller. 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)