proposition: Lemma aleph_pr12e x: ordinalp x -> \aleph (osucc x) <c \2c ^c (\2c ^c (\aleph x)).
proof: Proof. move => ocx;move: (CIS_aleph ocx); set E:= \aleph x => ife. suff: \omega (osucc x) <=c (\2c ^c E). move => h; apply: (cle_ltT h); apply: (cantor (proj32 h)). rewrite - (cnextE ocx); apply:cnext_pr3; apply:(CS_aleph ocx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)