proposition: Lemma infinite_power7g x y: infinite_c x -> x <=c y -> x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
proof: Proof. move => icx xy. have [cx cy _]:= xy. have icy: infinite_c y by apply: (cle_inf_inf icx xy). have ynz: y <> \0c by apply: infinite_nz. have x2: \2c <=c x by apply: infinite_ge2. rewrite (infinite_power1_a (infinite_ge2 icx) xy icy) /csumb. have pa:= cleT xy (proj1 (cantor cy)). move: (infinite_power7d (proj1 icx) (infinite_nz icx)) => [pb pc]. set f := Lg _ _. have cf: fgraph f by rewrite /f; fprops. have pd: infinite_c (\2c ^c y) by apply: (cle_inf_inf icx pa). have fl: forall i, inc i (domain f) -> Vg f i <=c \2c ^c y. rewrite /f; aw; move=> i idf; rewrite LgV//. move: idf => /(cardinals_ltP cx) idf. have p1:= (proj1 (clt_leT idf xy)). case: (equal_or_not i \0c) => iz. rewrite iz (cpow0x ynz); apply: cle0x; fprops. case: (equal_or_not i \1c) => io. by rewrite io (cpow1x); apply: (cle_fin_inf finite_1). have i2:= (cge2 (proj31 p1) iz io). rewrite (infinite_power1_a i2 p1 icy). apply: cleR; rewrite /cpow; fprops. move: (csum_of_small_b1 (conj cf fl)); rewrite {2} /f; aw. rewrite - cprod2cr => le2. have le3:= (cleT le2 (cprod_inf1 (cleT pb pa) pd)). apply:cleA; last by apply: cprod_inf4. apply: cleT (cprod_M1le (proj31 le3) (infinite_nz icx)). have d2: inc \2c (cardinals_lt x). apply/(cardinals_ltP cx). apply: (clt_fin_inf finite_2 icx). move:(proj1 pd). have ->: \2c ^c y = Vg f \2c by rewrite /f LgV. by move => cc;apply(csum_increasing6 cc); rewrite/f Lgd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)