proposition: Lemma regular_initial_limit0 x: limit_ordinal x -> \cf (\aleph x) <=o \cf x.
proof: Proof. move => lx; move: (lx) => [ox _ _]; move: (CIS_aleph ox) => icx. rewrite - (cofinality_card icx). move: (cofinality_c_rw (infinite_ge2 icx)) => [pa pb pc]. move: (cofinality_rw ox)=> [pd [f [[ff sf tf] cf]] _]. set E:= Imf f. have Ex: sub E x by rewrite -tf; apply: Imf_Starget. have se: union E = x. set_extens t. move => /setU_P [ z tz /Ex zx]; exact:(ordinal_transitive ox zx tz). move/(proj33 lx) /cf => [z za /oleSltP zb]; apply /setU_P. exists (Vf f z); first by move/oltP0: zb => [_ _]. apply /Imf_P => //; exists z => //; ue. have oce: ordinalp (cardinal E) by apply: OS_cardinal; fprops. have pe: csum_of_small1 (\omega x) (Lg E \omega). split; fprops; hnf;aw => t tdf; rewrite LgV//; apply aleph_lt_ltc. by apply /(oltP ox); apply: Ex. have pf: cofinality_c_ex (\omega x) (cardinal E). move: (csum_commutative1 pe) => [g [ga gb gc gd]]; exists g; split => //. by rewrite gb; aw. by rewrite - gc (aleph_sum_pr4 lx Ex se). move: (pc _ oce pf). move: (image_smaller ff); rewrite -/E sf. rewrite (card_card (CS_cofinality ox)) => c1 c2 . exact: (oleT c2 (ocle c1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)