proposition: Lemma cpow_less_pr7a x: infinite_c x -> csumb (cardinals_le x) (fun t => x ^c t) = \2c ^c x.
proof: Proof. move => icx; move: (icx) => [cx _]. set f := (Lg (cardinals_le x) [eta cpow x]). set a := cardinals_lt x. have h1P:= (cardinals_ltP cx). have h2P:= (cardinals_leP cx). have fgf: fgraph f by rewrite /f; fprops. have pa: (a +s1 x) = (domain f). rewrite /f /a; aw; set_extens t. case/setU1_P => ha;apply /h2P; [by move/h1P: ha => []| rewrite ha; fprops]. move /h2P=> aux; apply /setU1_P; case:(equal_or_not t x) => tx; [by right |]. by left ; apply /h1P; split. have pb: sub (a +s1 x) (domain f) by rewrite pa; fprops. have pc: ~(inc x a) by move /h1P => [_]. move: (induction_sum0 f pc). rewrite pa (restr_to_domain fgf (@sub_refl f)) /csumb; move => ->. have pd : inc x (cardinals_le x) by apply/ h2P; fprops. have ->: (restr f a) = Lg a (cpow x). apply: Lg_exten => t tx; rewrite /f LgV//. move: pa; rewrite /f Lgd;move => <-; fprops. rewrite -/(csumb _ _) - (cpow_less_alt icx (infinite_ge2 icx)). move: (cpow_less_compare icx) => [_ [_ pe]]. rewrite /f LgV//-(infinite_power1_b icx). rewrite csumC (csum_inf pe) //; apply: CIS_pow => //. by apply: infinite_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)