proposition: Lemma total_order_length r: order r -> finite_set (substrate r) -> (order_length r (cardinal (substrate r)) <-> total_order r).
proof: Proof. move => or fse. split => hyp; last first. split. exists (substrate r) => //; apply /total_subordersP; split => //. by apply:total_order_sub. by move => x /total_subordersP [] /sub_smaller. move: (proj1 hyp) => [X /total_subordersP [Xsr Xt] cX]. by move: Xt; rewrite (cardinal_setC5 fse Xsr cX) iorder_substrate. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)