proposition: Lemma infinite_power6_7d: \aleph omega0 <c \2c ^c omega0 -> (\aleph omega0) ^c omega0 = \2c ^c omega0.
proof: Proof. move=> [h _ ]. move: (CIS_aleph OS_omega) => io. apply: cleA; last first. apply cpow_Mleeq;[ by apply: infinite_ge2 | fprops]. move: (cpow_Mleeq omega0 h (infinite_nz io)). rewrite - cpow_pow csquare_inf //; apply: CIS_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)