proposition: Lemma next_fix_point_small1 f C x (E:= cnext C) (y:= the_least_fixedpoint_ge (Vf f) x): infinite_c C -> normal_function f E E -> inc x E -> [/\ x <=o y, inc y E, Vf f y = y & (forall z, x <=o z -> inc z E -> Vf f z = z -> y <=o z)].
proof: Proof. move => icE nf xE. have [pa pb pc]:= (cnext_pr1 (proj1 icE)). have [qa qb qc qd] := (induction_defined_pr (Vf f) x). move: (image_smaller (proj1 qb));rewrite qa (surjective_pr0 qb)=> sa. have fee: (forall x, inc x E -> inc (Vf f x) E). move:nf => [[ff sf tf] pd pe]. rewrite -{1} sf - tf => t tsf; Wtac. have ye: inc y E. apply: cnext_sup => //. by apply: (cleT sa); rewrite cardinal_Nat; apply /infinite_c_P2. move => t /(proj2 qb); rewrite qa; move => [z zN ->]; move: z zN. apply: Nat_induction; first by rewrite qc. move => n nN /fee hr; rewrite qd //. have [oe _] := (pa). have xe: x <o E by apply/oltP. case: (normal_function_fix nf xe); rewrite -/y. by move => yee; move:ye; rewrite yee; move: (ordinal_irreflexive oe). by move => [ta tb tc td]; split => // z xz ze; apply: td => //; apply/oltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)