proposition: Lemma iclosed_lim: iclosed_proper limit_ordinal.
proof: Proof. split; last first. apply:unbounded_non_coll => x ox; exists (x +o omega0). exact: (osum_Mle0 ox OS_omega). exact:(osum_limit ox omega_limit ). split; first by move => x []. move => F fl nef. have os: ordinal_set F by move => x /fl []. case: (ord_sup_inVlimit os nef); [ by move /fl | done]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)