proposition: Lemma infinite_power6 p m (y:= \aleph p): ordinalp p -> m <> \0o -> cardinal p <=c m -> (infinite_c m \/ p <> \0o) -> y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
proof: Proof. move=> op mz cpm dc. have cm := proj32 cpm. move: (infinite_power5 OS0 op mz cpm). rewrite (osum0l op) -/y aleph0E; move => ->. have pa:= CIS_omega. have aux:=(infinite_ge2 pa). case: (finite_or_infinite cm) => fm; last first. move/infinite_c_P2:(fm) => fm'. by rewrite (infinite_power1_a aux fm' fm). case: dc => pz; first by case: (finite_not_infinite fm pz). have mb: natp m by apply /NatP. have mpb: natp (cardinal p) by apply (NS_le_nat cpm mb). rewrite (cpow_inf pa mb mz). have iy:= (CIS_aleph op). rewrite (cpow_inf iy mpb (card_nonempty0 pz)). have le1: omega0 <=c \aleph p. by rewrite - aleph0E; apply: aleph_le_lec; by apply: ole0x. have le2: \2c ^c m <=c \aleph p. apply: cleT le1. apply: cle_fin_inf => //;apply /NatP; apply: NS_pow; fprops. rewrite cprodC (cprod_inf le1 iy omega_nz). by rewrite cprodC (cprod_inf le2 iy (@cpow2_nz m)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)