proposition: Lemma regular_initial_limit1 x: limit_ordinal x -> \cf (\aleph x) = \cf x.
proof: Proof. move=> lx; apply: oleA; first by apply: regular_initial_limit0. move: (lx) => [ox _ _]. pose thei t := Yo (infinite_c t) (ord_index t) \0o. rewrite - (cofinality_card (CIS_aleph ox)). have thei1: forall t, infinite_c t -> (ordinalp(thei t) /\ \aleph (thei t) = t). by move=> t it; rewrite /thei; Ytac0; apply: ord_index_pr1. have the2: forall t, t <c (\aleph x) -> thei t <o x. move=> t to; case: (p_or_not_p (infinite_c t)) => ti. move: (thei1 _ ti) => [ot eq]; rewrite - eq in to. apply: (aleph_ltc_lt ot ox to). by rewrite /thei; Ytac0; move: lx => [p1 p2 _]; apply /oltP. move: (cofinality_c_rw (infinite_ge2 (CIS_aleph ox))) => [pa pb _]. move: pb => [f [ [qa qb] qc qd]]. pose g := Lf (fun i => thei (Vg f i)) (domain f) x. have the3: forall u, inc u (domain f) -> thei (Vg f u) <o x. by move => i idf; apply: the2; apply: qb. have ga: lf_axiom (fun i => thei (Vg f i)) (domain f) x. by move => i /=; aw => idf; apply /(oltP ox); apply: the3. have fg: function g by apply: lf_function. set z := \osup (Imf g). move: (cofinality_rw ox) => [pc _ pd]. have oT: ordinal_set (Imf g). move=> t /(Imf_Starget fg); rewrite /g; aw;exact: (Os_ordinal ox). case: (equal_or_not z x) => zx. apply: pd. exact: (proj31 (ocle pa)). rewrite -qc; exists g; split; first by split => //; rewrite /g; aw. move=> t /(oltP ox) tx; ex_middle bad. suff xt: x <=o t by case: (oltNge tx). move: (proj31_1 tx) => ot;rewrite - zx;apply: ord_ub_sup => //. move=> i ia; move: ia (oT _ ia). move /(Imf_P fg);rewrite {1}/g; aw; move=> [u usg ->] ow. case: (oleT_el ow ot) => //; move=> [le1 _];case: bad; ex_tac. have lezx: z <o x. split => //; apply: ord_ub_sup => //. move => i /(Imf_P fg). rewrite /g; aw; move=> [u usg ->]; rewrite LfV//; exact: (proj1 (the3 _ usg)). have oz:=proj31_1 lezx. have th4: forall i, inc i (domain f) -> Vg f i <=c (\aleph z). move=> i idf. case: (finite_or_infinite (proj31_1 (qb _ idf))) => fd. move: (CIS_aleph oz) => le2; exact: (cle_fin_inf fd le2). move:(thei1 _ fd) => [pe <-]; apply: aleph_le_lec. have ->: thei (Vg f i) = Vf g i by rewrite /g LfV//. apply: ord_sup_ub => //; apply /(Imf_P fg). by exists i => //; rewrite /g; aw. move: (csum_of_small_b1 (conj qa th4)); rewrite qc qd. move: (aleph_lt_ltc lezx) pa. set A := \aleph x; set B := \aleph z; set C := cofinality_c (\aleph x). move => le1 pa le2. have cb := proj31_1 le1. have cc:= proj31 pa. have anz: A <=c \0c -> False. move: (CIS_aleph ox) => ia h. have fz: finite_c \0c by apply: finite_0. case: (cleNgt h (clt_fin_inf fz ia)). move: (CIS_aleph oz) => ib. case: (equal_or_not C \0c) => cz. by move: le2; rewrite cz cprod0r => h; case: anz. case: (cleT_ee cb cc) => auc; last first. move: (cprod_inf auc ib cz) => xx. by case:(cltNge le1); rewrite -xx. move: (cle_inf_inf ib auc) => ic. move: (cprod_inf auc ic (aleph_nz oz)). rewrite cprodC => xx; rewrite xx in le2. apply: (oleT (cofinality_pr3 ox)). rewrite (cleA pa le2). by apply: aleph_pr6. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)