proposition: Lemma regular_initial_successor x: ordinalp x -> regular_cardinal (\aleph (osucc x)).
proof: Proof. move => ox. have osx:= (OS_succ ox). have iy:= (CIS_aleph osx). have y2:= (infinite_ge2 iy). move: (cofinality_c_rw y2) => [pc [f [fa fb fc] _]]. split => //; case:(cle_eqVlt pc) => //. rewrite - (card_card (CS_cofinality_c (proj1 iy))) - fb => h. have en: (exists2 n, ordinalp n& \aleph (osucc x) = \aleph (osucc n)) by exists x. by case: (proj2(csum_of_small_b3 fa en h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)