proposition: Lemma cnextP c: cardinalp c -> forall x, (inc x (cnext c) <-> (ordinalp x /\ cardinal x <=c c)).
proof: Proof. move => cc x. move:(cantor cc) => ncc; move: (ncc) => [[_ cc1 _] _]; move: (cc1) => [oc _]. split; first by move /Zo_P =>[/(Os_ordinal oc) h1 h2]. move => [h1 h2];apply: Zo_i => //. move: (cle_ltT h2 ncc) => h3. by move /(ocle2P cc1 h1): h3 => /oltP0 []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)