proposition: Lemma aleph_pr10a x y: ordinalp x -> y <c \aleph (osucc x) -> y <=c \aleph x.
proof: Proof. move => ox lt1; move: (lt1) => [[cy cso _] _]. case: (cleT_el cy (CS_aleph ox)) => // pc. have iy := (cle_inf_inf (CIS_aleph ox) (proj1 pc)). move: (ord_index_pr1 iy) lt1 => [ox' <- /(aleph_ltc_lt ox' (OS_succ ox))]. by move /oltSleP/aleph_le_lec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)