proposition: Lemma infinite_power7f1 a y: limit_ordinal a -> y <c \cf a -> y <> \0c -> (\aleph a) ^c y = csumb a (fun z => (\aleph z) ^c y).
proof: Proof. move => pa pb pc. have on:= (proj31 pa). move: (infinite_power7f pa pb); rewrite - Lg_range=> eq0. move: (ocle1 (aleph_pr6 on)); rewrite (card_card (CS_aleph on)) => le2. rewrite eq0;symmetry; apply: csum_of_small_b4. - fprops. - by hnf; aw; move=> i an; rewrite LgV//; fprops. - by rewrite - eq0; apply: CIS_pow => //; apply: CIS_aleph. - by rewrite - eq0 Lgd; exact: (cleT le2 (cpow_Mle1 (proj32 le2) pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)