proposition: Lemma infinite_power6_6 n : ordinalp n -> \2c ^c (\aleph omega0) = \aleph (\omega n) -> omega0 <o n.
proof: Proof. move => on h3; symmetry in h3. exact (infinite_power6_5 on OS_omega h3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)