proposition: Lemma infinite_power6_1 a: a <o omega1 -> (\aleph a) ^c aleph1 = (\aleph a) ^c aleph0 *c \2c ^c aleph1.
proof: Proof. move => ao. have oa:= proj31_1 ao. have ica:=(CIS_aleph OS1). move: ao => /(ocle2P (proj1 ica) oa) ao. rewrite /aleph0 - aleph0E. move: (aleph_nz oa) => xnz. apply: cleA. rewrite (infinite_power6_0 oa ica (proj1 ao)) cprodC. apply: cprod_Mlele; last by apply: cleR; fprops. by apply: cpow_Meqle => //;apply: (aleph_pr10a OS0); rewrite osucc_zero. have ioa:= (CIS_aleph oa). apply: cprod_inf4. - apply: cpow_Meqle => //; apply: aleph_le_lec; apply: ole0x; fprops. - apply: cpow_Mleeq; [ apply: cle_fin_inf | ]; fprops. - apply: CIS_pow => //; apply: aleph_nz; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)