proposition: Lemma regular_finite x: regular_ordinal x -> [\/ x = \0o, x = \1o | omega0 <=o x].
proof: Proof. move => [ox rx]. case: (ordinal_limA ox) => aux; first by constructor 1. constructor 2. move: aux => [y _ xs]. move:rx; rewrite {1} xs cofinality_succ //; apply: OS_succr; ue. constructor 3;exact (limit_ge_omega aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)