proposition: Lemma cofinality_prod_omega a: \0o <o a -> \cf (a *o omega0) = omega0.
proof: Proof. move => oa. rewrite (cofinality_prod oa omega_limit); exact: (proj2 regular_omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)