proposition: Lemma aleph_pr12c x z: ordinalp x -> ordinalp z -> cardinal z <=c \aleph x -> z <o \aleph (osucc x).
proof: Proof. move=> ox oz p1; move: (p1) => [_ cy _]. rewrite - (cnextE ox); apply /(oltP (proj1 (CS_cnext cy))). by apply/cnextP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)