proposition: Lemma infinite_power2 n m (x:=\aleph n) (y:= \aleph (osucc n)): ordinalp n -> m <> \0c -> y ^c m = (x ^c m) *c y.
proof: Proof. move => on mnz. rewrite -(cpowcr) -(cpowcr x);set m':= cardinal m. have cm': cardinalp m' by rewrite /m'; fprops. have m'nz:=(card_nonempty0 mnz). have osn:= (OS_succ on). move: (CIS_aleph on) (CIS_aleph osn) (aleph_pr10c on). rewrite -/x -/y => icx icy ap. have m1: \1c <=c m' by apply: cge1; fprops. have p1: forall z, ordinalp z -> (\aleph z) <=c ((\aleph z) ^c m'). move=> z oz; move: (CIS_aleph oz) => iz; move: (iz) => [cz _]. apply: cpow_Mle1 => // coz. have ipx: infinite_c (x^c m') by apply: (CIS_pow). move: (ap) => [lexy _]. have cxy := (cpow_Mleeq m' (proj1 ap) (aleph_nz on)). move: (icy) => [cy _]; move:(cy) => [oy _]. apply: cleA; last first. by apply: cprod_inf4 => //; [apply: p1 | apply:CIS_pow]. case: (cleT_el cy cm') => cmx. have im:= (cle_inf_inf icy cmx). have lex2:=(infinite_ge2 icx). rewrite (infinite_power1_a lex2 (cleT lexy cmx) im). rewrite (infinite_power1_a (cleT lex2 lexy) cmx im). apply: cprod_M1le => //; fprops. apply: (aleph_nz (OS_succ on)). have ha: m' <c \cf y. by move: (regular_initial_successor on) => /regular_cardinalP [_ ->]. have hb:= (infinite_power7b icy ha). apply: (cleT hb); apply: (cleT (csum_pr1 (Lg y (functions m')))). rewrite /csumb; aw; set f := Lg _ _. have df: domain f = y by rewrite /f; aw. rewrite - df /f; apply:csum_of_small_b1. split; [ fprops | hnf; aw; move =>i ix; rewrite !LgV//]. rewrite -/(cpow i m') - cpowcl. case: (equal_or_not (cardinal i) \0c) => iz. by rewrite iz (cpow0x m'nz);apply: cle0x; rewrite /cpow; fprops. by apply: (cpow_Mleeq _ _ iz);apply: (aleph_pr12d on); apply /(oltP oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)