proposition: Lemma cardinal_pr1 x: cardinal_prop x (cardinal x).
proof: Proof. have [wor sr] :=(proj1 (Zermelo_ter x)). have [_ _ [bf sf tf] ff]:= (ordinal_isomorphism_exists wor). apply: (least_ordinal1 (OS_ordinal wor)); exists (ordinal_iso (worder_of x)). by split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)