proposition: Lemma infinite_power5' n p m (x:=\aleph n) (y:= \aleph (n +o p)): ordinalp n -> natp p -> m <> \0o -> p <=c m -> y ^c m = (x ^c m) *c y.
proof: Proof. move => pa pN pd pe. case: (equal_or_not p \0c) => pz. have ix:= CIS_aleph pa. have le1:=(cpow_Mle1 (proj1 ix) pd). have ipo:= (cle_inf_inf ix le1). by rewrite /y pz (osum0r pa) -/x (cprod_inf le1 ipo (infinite_nz ix)). have pb:= (OS_nat pN). have cp:=(card_card (CS_nat pN)); rewrite - cp in pe pN pz. rewrite (infinite_power5 pa pb pd pe). by rewrite (cpow_inf (CIS_aleph (OS_sum2 pa pb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)