proposition: Lemma omega_P2 x: inc x omega0 <-> finite_o x.
proof: Proof. split. move => xo; have ox:= (Os_ordinal OS_omega xo). split=>// /(omega_P1 ox) h. case: (ordinal_irreflexive ox (h _ xo)). by move => [ox /(omega_P1 ox) nifx]; case:(oleT_si OS_omega ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)