proposition: Lemma OIS_limit x: limit_ordinal x -> infinite_o x.
proof: Proof. move=> xl. have hh : z_infinite x by move: xl => [qa qb qc]; split => //. move: (z_omega_infinite2 hh) => qd. exact: (OIS_le_inf (proj2 (z_omega_limit hh) _ xl) qd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)