proposition: Lemma normal_function_fixpoints x f: ordinalp x -> normal_function f x x -> (\cf x <> omega0) -> (forall a, inc a x -> exists b, [/\ inc b x, a <=o b & Vf f b = b]).
proof: Proof. move=> ox nf cfx a ax. move/(oltP ox) :ax => ax1. move: (normal_function_fix nf ax1); set y := the_least_fixedpoint_ge _ _. case; last by move => [ay /(oltP ox) yx fy _]; ex_tac. move => yx; case: cfx. move:nf => [[ff sf tf] sif nff]. move: (induction_defined_pr (Vf f) a). set g := induction_defined (Vf f) a; move=> [sg [fg sjg] gz gnz]. have xi: inc a (target g) by rewrite -gz; Wtac; rewrite sg; apply:NS0. have ne: nonempty (target g) by exists a. have lt1: forall n, natp n -> Vf g n <o x. apply: Nat_induction; first by rewrite gz. move=> n nB; rewrite (gnz _ nB) => /(oltP ox) pd; apply /(oltP ox). rewrite - tf;Wtac. 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). by rewrite sg in sjg; move => /sjg [j /lt1 [_ xx] eq]; case: xx; rewrite - eq. rewrite /g -/( the_least_fixedpoint_ge _ _) -/y yx => ly. set g0:= Lf (Vf g) omega0 x. have cg: cofinal_function g0 x omega0. have la: lf_axiom (Vf g) omega0 x by move => t /lt1 /(oltP ox). rewrite /g0; split; first by saw; apply: lf_function. move=> t ty; ex_middle tm. have ot: ordinalp t by apply: (Os_ordinal ox ty). suff e: x <=o t by move: ty =>/(oltP ox)/(oleNgt e). rewrite - yx;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 ox) => [pd pe pf]. have pg: (cofinal_function_ex x 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)