proposition: Lemma regular_omega: regular_ordinal omega0.
proof: Proof. move: OS_omega => oo; split => //; apply: oleA. exact (cofinality_pr3 oo). exact: (cofinality_limit4 omega_limit). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)