proposition: Lemma aleph0E: \omega \0o = omega0.
proof: Proof. have icx:= iclosed_non_coll_infinite_c. have [ir lr]:=(iclosed_col_f0 icx). exact: (extensionality (proj33 (lr _ CIS_omega)) (omega_limit3 ir)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)