proposition: Lemma infinite_power6_ct p m (y:= \aleph p): ordinalp p -> infinite_c m -> cardinal p <=c omega0 -> y ^c m = (\2c ^c m) *c (y ^c aleph0).
proof: Proof. move => ha hb hc. move /infinite_c_P2: (hb) => hb'; move: (cleT hc hb') => hd. rewrite (infinite_power6_0 ha hb hd). case: (cle_eqVlt hc); first by move ->. case: (equal_or_not p \0c) => epz. have he:= (infinite_pow2 hb). rewrite /y epz cardinal_set0 cpowx0 /aleph0 aleph0E (cprod1r (proj1 he)). by rewrite(infinite_power1_b CIS_omega) - cpow_sum2 csum_inf. move/clt_omegaP => nn. have pN: natp p by apply/NatP;apply:(ordinal_finite1 ha); apply/NatP. rewrite (cpow_inf (CIS_aleph ha) nn (card_nonempty0 epz)). by rewrite (infinite_power3 pN omega_nz) cprodA - cpow_sum2 (csum_inf hb' hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)