proposition: Lemma infinite_power6_0 p m (y:= \aleph p): ordinalp p -> infinite_c m -> cardinal p <=c m -> y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
proof: Proof. move=> op icm cp. exact: (infinite_power6 op (infinite_nz icm) cp (or_introl icm)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)