proposition: Lemma limit_ge_omega x: limit_ordinal x -> omega0 <=o x.
proof: Proof. move=> ln;move: OS_omega (ln) => oo [ox _ _]. by move /(omega_P1 ox):(OIS_limit ln); split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)