proposition: Lemma cofinality_least_fp_beth x y: beth x <> x -> least_fixedpoint_ge beth x y -> cofinality y = omega0.
proof: Proof. apply: (cofinality_least_fp_normal beth_normal). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)