proposition: Lemma aleph_pr10b x y: ordinalp x -> \aleph x <c y -> \aleph (osucc x) <=c y.
proof: Proof. move=> ox h. case: (cleT_el (CS_aleph (OS_succ ox)) (proj32_1 h)) => // pc. case: (cltNge h (aleph_pr10a ox pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)