proposition: Lemma cardinal_pr3 a: ordinalp a -> cardinal a <=o a.
proof: Proof. move => oa. by have [h1 h2]:=(CS_cardinal a); split => //; apply/(h2 _ oa)/card_eqP; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)