proposition: Lemma normal_function_fix f a x (y:= the_least_fixedpoint_ge (Vf f) x): normal_function f a a -> x <o a -> (y = a \/ [/\ x <=o y, y <o a, Vf f y = y & (forall z, x <=o z -> z <o a -> Vf f z = z -> y <=o z)]).
proof: Proof. move=> nf lxa. have [[ox oa _] _] := lxa. move:NS0 => ns0. have aux: forall x, x <o a -> x <=o (Vf f x) /\ Vf f x <o a. by move => t ta; apply: normal_fn_unbounded. move: (induction_defined_pr (Vf f) x). set g := induction_defined (Vf f) x; move=> [sg sjg gz gnz]. have fg: function g by fct_tac. move: (nf) => [[ff sf tf] sif nf0]. have pb: forall i, inc i (target g) -> x <=o i /\ i <o a. move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg ->]. move: j jsg; rewrite sg; apply: Nat_induction. rewrite gz; split => //; apply: (oleR ox). move=> n nN; rewrite (gnz _ nN); move => [p1 p2]. move: (aux _ p2) => [s1 s2]; split => //; apply: (oleT p1 s1). have osg: ordinal_set (target g) by move => i /pb [_][[]]. have sta: sub (target g) a by move => t /pb [_] /(oltP oa). have netg: nonempty (target g) by exists (Vf g \0c); Wtac; rewrite sg. have sa: x <=o y. by apply :ord_sup_ub => //; rewrite - /g - gz; Wtac; rewrite sg. have sb: y <=o a by apply :ord_ub_sup => // i /pb [_ []]. case: (equal_or_not y a) => eya; [by left | right;split => //; last first]. move => z xz za fz. have oz:= proj32 xz. apply: ord_ub_sup => //. move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg ->]. move: j jsg; rewrite sg; apply: Nat_induction; first by rewrite gz. move=> n nN; rewrite (gnz _ nN) => p1; rewrite - fz. case: (equal_or_not ( Vf g n) z) => neq; first by rewrite neq fz; apply:oleR. have ha: inc (Vf g n) a by apply /(oltP oa); apply: (ole_ltT p1 za). have hb: inc z a by apply/(oltP oa). exact (proj1(sif (Vf g n) z ha hb (conj p1 neq))). move: (aux _ (conj sb eya)) => [sc sd]. apply: oleA => //. move: (sta); rewrite - sf => stf. have ha: ordinal_set (Vfs f (target g)). by move => t /(Vf_image_P ff stf) [u /pb [_ /aux [_ [[oo _ _] _] ->]]]. case: (normal_function_equiv oa oa nf sta netg) => //; rewrite -/y => ->. apply: ord_ub_sup => //; first by case:sa. move => t /(Vf_image_P ff stf) [u utg ->]. move: (proj2 sjg _ utg)=> [v va ->]. rewrite sg in va; rewrite - (gnz _ va); apply :ord_sup_ub => //. by rewrite -/g; Wtac; rewrite sg; apply:NS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)