proposition: Lemma regular_initial_limit3 x: limit_ordinal x -> x <o \aleph x -> singular_cardinal (\aleph x).
proof: Proof. move=> pa pb; move: (regular_initial_limit2 pa) => pc. split; first by apply: (CIS_aleph (proj31 pa)). by move: (ole_ltT pc pb) => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)