proposition: Lemma infinite_power6_7b: \2c ^c aleph1 = aleph2 -> (\aleph omega0) ^c aleph0 <> \aleph omega1.
proof: Proof. move => pa pb. move: (esym (infinite_power6_7a pa)); rewrite pb => aux. by case: (proj2(infinite_power6_5 OS1 OS1 aux)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)