proposition: Lemma regular_initial_limit5 x: singular_cardinal x -> (\aleph omega0) <=c x.
proof: Proof. move=> sx; move: (sx) => [ix _]. move: (sx) => [_]; rewrite -(cofinality_card ix). move: (ord_index_pr1 ix) => [on <-] nr; apply: aleph_le_lec. case: (ordinal_limA on) => h. - case: nr; rewrite h aleph0E; exact:(proj2 regular_cardinal_omega). - move:h=> [m om nsy]. case: nr; rewrite nsy; exact: (proj2 (regular_initial_successor om)). - by apply: limit_ge_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)