proposition: Lemma cardinalP x: cardinalp x <-> (ordinalp x /\ forall z, inc z x -> ~ (x \Eq z)).
proof: Proof. rewrite /cardinalp; split; move=> [ox h]; split => //. move => z zx ne; move: ((h _ (Os_ordinal ox zx) ne) _ zx). apply: (ordinal_decent ox zx). move=> z oz exz. case: (ordinal_inA oz ox) => ty; first by case: (h _ ty). by apply: (ordinal_transitive oz). by rewrite ty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)