proposition: Lemma infinite_power7 x y: infinite_c x -> y <c \cf x -> y <> \0c -> x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
proof: Proof. move=> pa pb pc. have cy:= proj31_1 pb. have cx:= proj1 pa. have le1:= (infinite_power7b pa pb). have le2:= (infinite_power7c cx cy). apply: (cleA (cleT le1 le2)). have pd:= (cpow_Mle1 cx pc). have ip:=(cle_inf_inf pa pd). apply: (cprod_inf4 _ pd ip). set f := (Lg (cardinals_lt x) (cpow^~ y)). have fl: (forall i, inc i (domain f) -> Vg f i <=c x ^c y). rewrite /f; aw; move=> i id; rewrite LgV//. case: (equal_or_not i \0c) => iz. rewrite iz (cpow0x pc);apply: (cle0x (proj32 pd)). move: id => /(cardinals_ltP cx) [le _]. by apply: cpow_Mleeq. move: (infinite_power7d cx (infinite_nz pa)) => [pe1 pf]. have fgf: fgraph f by rewrite /f; fprops. move: (csum_of_small_b1 (conj fgf fl)); rewrite {2}/f; aw. rewrite - cprod2cr cprod_inf//; exact: (cleT pe1 pd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)