proposition: Lemma singular_limit n: ordinalp n -> singular_cardinal (\aleph n) -> limit_ordinal n.
proof: Proof. move => on [pa pb]. case: (ordinal_limA on) => li //. by move: pb; rewrite li aleph0E (proj2 (regular_omega)). move:li => [c oc cv]. by move:(regular_initial_successor oc) => /regular_cardinalP [_]; rewrite - cv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)