proposition: Lemma infinite_power3 n m (x:=\aleph n): natp n -> m <> \0c -> x ^c m = (\2c ^c m) *c x.
proof: Proof. move=> nN mz. rewrite - (cpowcr x m) - (cpowcr \2c m). set m':= cardinal m. have cm': cardinalp m' by rewrite /m'; fprops. have m'nz:= (card_nonempty0 mz). rewrite /x; clear x. case: (finite_or_infinite cm') => fm. have mN: natp m' by apply /NatP. have on:=(OS_nat nN). have io:=(CIS_aleph on). rewrite (cpow_inf io mN m'nz) cprodC. symmetry; apply: cprod_inf => //; last by apply: cpow2_nz. apply: cle_fin_inf => //. apply /NatP; apply: NS_pow; fprops. have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops. have pa: \2c <=c omega0 by apply: infinite_ge2. have onz:= omega_nz. move: n nN; apply: Nat_induction. move: (infinite_pow2 fm) => px; move/infinite_c_P2: (px) => le2. rewrite aleph0E (infinite_power1_d fm) cprod_inf //. move=> n nN hrec. rewrite succ_of_finite; last by apply /NatP. have on:= (OS_nat nN). rewrite (infinite_power2 on m'nz) hrec - cprodA. have pc := proj1 (aleph_pr10c on). move: (cprod_inf pc (CIS_aleph (OS_succ on)) (aleph_nz on)). by rewrite cprodC; move => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)