proposition: Lemma infinite_power6_7f: \aleph omega0 <c (\aleph omega0) ^c aleph0 /\ \aleph omega1 <c (\aleph omega1) ^c aleph1.
proof: Proof. set x := \aleph omega0. set y := \aleph omega1. have icx: infinite_c x by apply: CIS_aleph; apply: OS_omega. have icy: infinite_c y by apply: CIS_aleph; apply: OS_aleph; fprops. have la: limit_ordinal omega1 by apply: aleph_limit; fprops. split. move: (power_cofinality1 icx). by rewrite (regular_initial_limit1 omega_limit) (proj2 (regular_omega)). move: (power_cofinality1 icy). move: (regular_cardinal_aleph1)=> [pa <-]. by rewrite (cofinality_card pa)(regular_initial_limit1 la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)