proposition: Lemma cofinality_least_fp_normal3 x y: ordinalp x -> least_fixedpoint_ge \omega (osucc x) y -> singular_cardinal y.
proof: Proof. move => ox pb. have pa: \omega (osucc x) <> (osucc x). move: (infinite_card_limit2 (CIS_aleph (OS_succ ox))). set z := \omega _; move => [/ordinal_irreflexive oz zz zs] zz1. case: oz; rewrite {1} zz1; apply: zs; rewrite zz1; fprops. case: (cofinality_least_fp_normal2 aleph_normal pa pb) => //. move => yo; move: pb => [_ fx _]; rewrite -fx yo. apply: regular_initial_limit4. move=> [pc pd]. have iy:infinite_c y by move: pb => [xx <- _]; apply: CIS_aleph. split => // aux; case: pd; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)