proposition: Lemma ocle2P x y: cardinalp x -> ordinalp y -> ((y <o x) <-> (cardinal y <c x)).
proof: Proof. move=> cx oy; rewrite -{2} (card_card cx). move: cx => [ox xp]. split; move => [p1 p2]. move: (ocle1 p1) => p5; split => //; dneg p3. by apply: (oleA p1); split => //; apply: (xp _ oy); apply/card_eqP. case: (oleT_el ox oy) => // p3. move: (ocle1 p3)=> r1;case: p2; apply:cleA p1 r1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)