proposition: Lemma infinite_power7h x y: regular_cardinal x -> \0c <c y -> x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
proof: Proof. move=> /regular_cardinalP [ic cfx] [[_ cy _] nzy]. case: (cleT_el (proj1 ic) cy) => xy; last first. rewrite - cfx in xy; exact: (infinite_power7 ic xy (nesym nzy)). by apply: infinite_power7g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)