proposition: Lemma infinite_power5'' n p m (x:=\aleph n) (y:= \aleph (n +o p)): ordinalp n -> natp p -> infinite_c m -> y ^c m = (x ^c m) *c y.
proof: Proof. move => pa pb pc. move:(Nat_hi pb) => pd. exact:(infinite_power5' pa pb (infinite_nz pc) (cle_fin_inf pd pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)