proposition: Lemma aleph_pr12d x z: ordinalp x -> z <o (\aleph (osucc x)) -> cardinal z <=c (\aleph x).
proof: Proof. move => ox lt1. have oz:= proj31_1 lt1. case: (cleT_el (CS_cardinal z) (CS_aleph ox)) => // h. case: (oltNge lt1 (aleph_pr12b ox oz h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)