proposition: Lemma ordinals_card_ltP y: cardinalp y -> forall x, inc x y <-> (ordinalp x /\ (cardinal x) <c y).
proof: Proof. move => cy x; move: (proj1 cy) => oy. split. move /(oltP oy) => xy;move: (proj31_1 xy) => ox;split => //. by apply /(ocle2P cy ox). by move => [ox]; move /(ocle2P cy ox) /(oltP oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)