proposition: Lemma cofinality_least_fp_normal x y f: normal_ofs f -> f x <> x -> least_fixedpoint_ge f x y -> \cf y = omega0.
proof: Proof. move=> nf fx [lexy fy fz]. move: (lexy) => [ox oy _]. move: (induction_defined_pr f x). set g := induction_defined f x; move=> [sg [fg sjg] gz gnz]. have yv : y = \osup (target g). move: (normal_ofs_fix nf ox) => [pa pb pc]. by apply: oleA; [apply:fz | apply: pc ]. have xi: inc x (target g) by rewrite -gz; Wtac; rewrite sg; apply:NS0. have ne: nonempty (target g) by exists x. have lt1: forall n, natp n -> Vf g n <o y. apply: Nat_induction. by rewrite gz; split => //; dneg xx; rewrite xx. by move=> n nB; rewrite (gnz _ nB) => pd; move: ((proj1 nf) _ _ pd); ue. have otg: ordinal_set (target g). move => t itg; move: (sjg _ itg) => [j jsg ->]. rewrite sg in jsg; exact:(proj31_1 (lt1 _ jsg)). case: (ord_sup_inVlimit otg ne); rewrite - yv. move => itg; move: (sjg _ itg). by rewrite sg; move=> [j jB eq]; move: (lt1 _ jB) =>[]; rewrite eq. move => ly. set g0:= Lf (Vf g) omega0 y. have cg: cofinal_function g0 y omega0. have la: lf_axiom (Vf g) omega0 y by move => t /lt1 /(oltP oy). rewrite /g0; split; first by saw; apply: lf_function. move=> t ty; ex_middle tm. have ot: ordinalp t by apply: (Os_ordinal oy ty). suff e: y <=o t by move: ty =>/(oltP oy) /(oleNgt e). rewrite yv;apply: ord_ub_sup => // i itg; move: (sjg _ itg). rewrite sg ; move => [u usg v]. have ow: ordinalp i by apply: otg. case: (oleT_ee ot ow) => // ti; case: (tm); exists u => //. by rewrite /g0 LfV// -v. move: (cofinality_rw oy) => [pd pe pf]. have pg: (cofinal_function_ex y omega0) by exists g0. move: (pf _ OS_omega pg) => le1. exact: (oleA le1(limit_ge_omega (cofinality_limit3 ly))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)