proposition: Lemma omega_P1 x: ordinalp x -> (infinite_o x <-> sub omega0 x).
proof: Proof. move=> ox; split; first by apply:(proj33 omega0_pr). move => sox; exact : (OIS_le_inf (And3 OS_omega ox sox) OIS_omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)