proposition: Lemma regular_initial_limit4: singular_cardinal (\aleph omega0).
proof: Proof. apply: regular_initial_limit3; first by apply: omega_limit. rewrite - {1} aleph0E. apply: aleph_lt_lto; apply/olt_omegaP; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)