proposition: Lemma cofinality_least_fp_normal2 x y f: normal_ofs f -> f x <> x -> least_fixedpoint_ge f x y -> y = omega0 \/ singular_ordinal y.
proof: Proof. move => pa pb pc; case: (equal_or_not omega0 y) => yno; first by left. right; rewrite /singular_ordinal /regular_ordinal. move:(pc) => [[_ oy _] _]; split => //. by rewrite (cofinality_least_fp_normal pa pb pc); move => [_ h]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)