proposition: Lemma infinite_power7h_rev x: \0c <c x -> (forall y, \0c <c y -> x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x) -> regular_cardinal x.
proof: Proof. move => xp h. move: (xp) => [_ /nesym xnz]. have cx:=proj32_1 xp. case: (equal_or_not x \1c) => x1. move: (h _ (clt_02)); rewrite x1 cpow1x; rewrite x1 in xp. have ->: (cardinals_lt \1c) = singleton \0c. apply : set1_pr; first by apply /(cardinals_ltP CS1). by move => t /(cardinals_ltP CS1) /clt1. rewrite csum_trivial3 (cpow0x card2_nz) (card_card CS0) cprod0l. by move => /card1_nz. case: (equal_or_not x \2c) => x2. move: (h _ (clt_02)); rewrite x2; rewrite x2 in xp. have ->: (cardinals_lt \2c) = C2. set_extens t. move => aux; apply /set2_P; apply: clt2. by apply /(cardinals_ltP CS2). case /set2_P => ->; apply /(cardinals_ltP CS2); [apply: clt_02 | apply: clt_12]. rewrite csum2_pr0 cpowx2 cprod_22 cpow1x (cpow0x card2_nz) (csum0l CS1). rewrite (cprod1l CS2) => eq3. by case: (proj2 (clt_leT (cltS NS2) (proj1 (cltS NS3)))). case: (Nat_dichot cx) => fx. move: (h _ (clt_01)); rewrite (cpowx1 cx) /csumb; set f := Lg _ _ => pb. have pa: \2c <=c csum f. have xx: inc \2c (cardinals_lt x). by apply /(cardinals_ltP cx); split; [ apply: cge2 | apply:nesym]. have i2d: inc \2c (domain f) by rewrite/f; aw. move: CS2;have ->: \2c = Vg f \2c by rewrite/f LgV// (cpowx1 CS2). move => cc; exact:(csum_increasing6 cc i2d). move: (cprod_Mlele pa (cleR cx)); rewrite -pb - csum_nn => qb. by move: (csum_Mlteq fx xp);rewrite (csum0l cx) => /(cleNgt qb). have H:= (cofinality_card fx). split => //. move: (cofinality_infinite fx); rewrite H => coi. move: (h _ (clt_fin_inf finite_0 coi)). rewrite /csumb; set f := Lg _ _. rewrite (infinite_power10_a fx) => pa. ex_middle cnx. have pc:= (cofinality_small fx). have pb: forall i, inc i (domain f) -> Vg f i <=c x. rewrite /f;aw;move=> i idf; rewrite LgV//. move: idf => /(cardinals_ltP cx) => idf. case: (equal_or_not i \0c) => i0. rewrite i0 cpow0x; [ exact (proj1 xp) | by apply: infinite_nz ]. case: (equal_or_not i \1c) => i1. by rewrite i1 cpow1x; apply (proj1 (infinite_gt1 fx)). have y2:= (cge2 (proj31_1 idf) i0 i1). have aux: forall z, infinite_c z -> z <c x -> \2c ^c z <=c x. move => z iz zx; rewrite - (gch iz). by move: (cnext_pr1 (proj1 iz)) => [_ _]; apply. case: (cleT_ee (proj31_1 idf) (proj31 pc)) => le1. by rewrite (infinite_power1_a y2 le1 coi); apply: aux. have iy:= (cle_inf_inf coi le1). move: (cpow_Meqle i0 le1); rewrite (infinite_power1_b iy) => ce. apply: (cleT ce (aux _ iy idf)). have cff: fgraph f by rewrite /f; fprops. move: (csum_of_small_b1 (conj cff pb)). rewrite Lgd. move: (infinite_power7d cx xnz) => [ca _]. move: (cprod_Mlele (cleR cx) ca); rewrite cprod2cr => cb cc. move: (cleT cc cb); rewrite (csquare_inf fx) => cd. move: (cprod_Mlele cd (cleR cx)); rewrite (csquare_inf fx) - pa. by move: (cnext_pr1 cx) => [_ aa _ ]=> /(cltNge aa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)