proposition: Lemma OT_nat_card n: natp n -> cardinal (substrate (OT_of_nat n)) = n.
proof: Proof. move => nN. move: (order_type_exists (ordinal_o_or n)) => [f [_ _ /equipotent_bp fp _] ]. by move/card_eqP:fp; rewrite ordinal_o_sr (card_card (CS_nat nN)); move <-. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)