proposition: Lemma cpow_less_ec_pr4 x y: infinite_c y -> \2c <=c x -> (exists a, cpow_less_ec_prop x y a) -> y <=c \cf (x ^<c y).
proof: Proof. move => icy x2 [a ha]. have hb:= (cpow_less_ec_pr2 ha x2). move: (ord_index_pr1 icy); set i := ord_index y; move=> [oi yv]. have xnz: \0c <c x by apply: clt_leT clt_02 x2. case: (ordinal_limA oi) => li. have yo: y = omega0 by rewrite -yv li aleph0E. move: ha => [ay h1]. rewrite (hb _ (cleR (proj31_1 ay)) ay). move: (oclt ay); rewrite yo => /olt_omegaP aN. have sN:= (NS_succ aN). have sy: (csucc a) <c y. rewrite yo; apply: clt_fin_inf => //; first by apply /NatP. apply: CIS_omega. have eq1:= (h1 _ (cleS aN) sy). case: (finite_or_infinite (proj32 x2)) => icx. have xN: natp x by apply /NatP. have x1:=(clt_leT (clt_12) x2). by move: (cpow_Meqlt xN sN (cltS aN) x1) => [_ bad]; case: bad. have pa:= (cofinality_infinite_cardinal (CIS_pow icx (@succ_nz a))). by rewrite eq1;apply /infinite_c_P2. move: li => [j oj jv]. have ->: y = cnext (\aleph j) by rewrite -yv jv cnextE. have ipy:= (CIS_aleph oj). rewrite (cpow_less_pr4 xnz ipy). by move: (power_cofinality5 x2 ipy)(cnext_pr1 (proj1 ipy)) => s [_ _]; apply. rewrite -yv. rewrite {1} (proj2 (aleph_normal) _ li). move: (ha) => [ay _]; move: (ay) => [[ca _] _ _]. have aa:= cleR ca. have [c [ic ac cy]]: exists c, [/\ infinite_c c, a <=c c & c <c y]. case: (finite_or_infinite ca); last by exists a. have io:= CIS_omega. move => fa; exists omega0; split => //; first by apply: cle_fin_inf. rewrite - aleph0E -yv; apply: aleph_lt_ltc. by move: li => [ori zi _]; apply/oltP. rewrite yv (hb _ ac cy). apply: card_ub_sup. apply: CS_cofinality; exact: (proj1 (CS_pow x c)). move => t /funI_P [z zi ->]. have zi1: z <o i by move: zi => /oltP []. move: (aleph_lt_ltc zi1); rewrite yv => lt. move: (ic) => [cc _]. case: (cleT_el cc (proj31_1 lt)) => le1. rewrite - (hb _ ac cy) (hb _ (cleT ac le1) lt). apply: (proj1 (power_cofinality5 x2 (CIS_aleph (proj31_1 zi1)))). exact:(cleT (proj1 le1) (proj1 (power_cofinality5 x2 ic))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)