proposition: Lemma cardinal_of_ordinal r: worder r -> (ordinal r) =c (substrate r).
proof: Proof. move=> wor; symmetry;apply /card_eqP. move: (ordinal_o_is wor) => [f [o1 o2 [bf pa pb] pc]]. by exists f; split => //; rewrite pb ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)