proposition: Lemma infinite_power6_4 a b: infinite_o a -> a <o omega1 -> ordinalp b -> (\aleph a) ^c (\aleph b) = (\aleph a) ^c aleph0 *c \2c ^c (\aleph b).
proof: Proof. move => ioa a1 ob. have oa:= proj31_1 a1. have iob:= (CIS_aleph ob). have eq1: cardinal a = \omega \0o. apply:cleA. apply/(aleph_pr10a OS0); rewrite osucc_zero. by move /(ocle2P (CS_aleph OS1) oa): a1. move:(infinite_set_pr2 ioa (ordinal_irreflexive oa)). rewrite aleph0E;apply/infinite_greater_countable1. move:(aleph_le_lec (ole0x ob)); rewrite - eq1 => ca2. by rewrite (infinite_power6_0 oa iob ca2) cprodC eq1 aleph0E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)