proposition: Lemma normal_ofs_fix1 f u x: normal_ofs1 f u -> u <=o x -> x <=o f x -> least_fixedpoint_ge f x (the_least_fixedpoint_ge f x).
proof: Proof. move=> nf0 ux xfx; rewrite /the_least_fixedpoint_ge. have ox:= proj31 xfx. move: nf0 => [sif nf]. have aux: forall t, x <=o t -> t <=o f t. by move => t; apply:(osi_gexu sif ux xfx). move: (induction_defined_pr f x). set g := induction_defined f x; move=> [sg sjg gz gnz]. have fg: function g by fct_tac. set y := \osup (target g). have pb: forall i, inc i (target g) -> x <=o i. move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg ->]. move: j jsg; rewrite sg; apply: Nat_induction. rewrite gz; apply: (oleR ox). move=> n nN; rewrite (gnz _ nN) => p1. exact: (oleT p1 (aux _ p1)). have pc: (forall i, inc i (target g) -> u <=o i). move=> i itg; exact: (oleT ux (pb _ itg)). have xi: inc x (target g) by rewrite -gz; Wtac; rewrite sg; apply:NS0. have ne: nonempty (target g) by exists x. have otg: ordinal_set (target g) by move=> t tg; case: (pb _ tg). split => //. - exact:(ord_sup_ub otg xi). - rewrite - (nf _ pc ne). apply: ord_sup_1cofinal; [ split | done]. move => t /funI_P [z ztg ->]. move: ((proj2 sjg) _ ztg) => [i isg ->]. by rewrite sg in isg; rewrite -gnz //; Wtac;rewrite sg; apply:NS_succ. move=> a atg. move: ((proj2 sjg) _ atg) => [i isg ->]. rewrite sg in isg. have wt: inc (Vf g i) (target g) by Wtac. exists (Vf g (csucc i)); rewrite (gnz _ isg). by apply /funI_P; exists (Vf g i). by apply: aux; apply: pb. - move => z xz fz. have oz: ordinalp z by case: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. have /pc le1 : inc (Vf g n) (target g) by Wtac; ue. case: (equal_or_not (Vf g n) z) => h; first by rewrite h fz; apply:oleR. rewrite - fz; exact: (proj1 (sif _ _ le1 (conj p1 h))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)