proposition: Lemma iclosed_nonlim: ~(iclosed_collection (fun z => ordinalp z /\ ~limit_ordinal z)).
proof: Proof. move: OS_omega omega_limit => ha hb. have pe: (forall x, inc x omega0 -> ordinalp x /\ ~ limit_ordinal x). move => x /(oltP ha) xo; have ox :=(proj31_1 xo). by split => // /limit_ge_omega /(oltNge xo). have pc: nonempty omega0 by exists \0o; apply: NS0. by move => [_ h]; case: (proj2 (h _ pe pc)); rewrite - [union _] omega_limit0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)