proposition: Lemma infinite_power6_2 b: b <o omega2 -> (\aleph b) ^c aleph2 = (\aleph b) ^c aleph1 *c \2c ^c aleph2.
proof: Proof. move => ao. have oa:= proj31_1 ao. have coo: cardinalp aleph2 by apply: CS_aleph; fprops. move: ao => /(ocle2P coo oa) ao. have xnz:= (aleph_nz oa). apply: cleA. rewrite (infinite_power6_0 oa (CIS_aleph OS2) (proj1 ao)) cprodC. apply: cprod_Mlele; last by apply: cleR; fprops. by apply: cpow_Meqle => //;apply: (aleph_pr10a OS1); rewrite osucc_one. have ioa:= (CIS_aleph oa). apply: cprod_inf4. - apply: cpow_Meqle => //;apply: aleph_le_lec;apply: oge1; fprops. - apply: cpow_Mleeq; [ apply: cle_fin_inf |];fprops. - apply: CIS_pow => //; apply: aleph_nz; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)