proposition: Lemma omax_p2 y (c:= cardinal (omax y omega0)): ordinalp y -> (infinite_c c /\ inc y (cnext c)).
proof: Proof. move:OS_omega => oo oy; move:(omax_p1 oy oo) => [pa pb]; split. by apply /infinite_c_P2; move: (ocle1 pb); rewrite cardinal_Nat. by apply /cnextP; [ rewrite /c; fprops | split=> //; apply: ocle1 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)