proposition: Lemma infinite_power6_7a: \2c ^c aleph1 = aleph2 -> \aleph omega0 ^c aleph1 = \aleph omega0 ^c aleph0.
proof: Proof. move => pa; move: infinite_power6_3; rewrite pa. have pc: aleph2 <=c \aleph omega0 ^c aleph0. have l1:= (aleph_le_lec ole_2omega). apply: (cleT l1 (cpow_Mle1 (proj32 l1) omega_nz)). have i2:=(CIS_aleph OS2). have i3:= (cle_inf_inf i2 pc). by rewrite (cprod_inf pc i3 (infinite_nz i2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)