proposition: Lemma first_derivation_p3 f x: normal_ofs f -> ordinalp x -> (first_derivation f (osucc x)) = the_least_fixedpoint_ge f (osucc (first_derivation f x)).
proof: Proof. move => nf ox; move:(iclosed_fixpoints nf) => [pa pb]. set p := (fun z : Set => ordinalp z /\ f z = z). have pc: forall y, p y -> ordinalp y by move=> y []. move: (ordinals_col_p1 pc pb) => [q1 q2 q3 q4 [q5 q6]]. rewrite /first_derivation -/p. move: (q1 _ ox) => [ta tb]. move: (normal_ofs_fix nf (OS_succ ta)) => [/oleSltP sa sb sc]. apply: oleA. move: (q2 _ (conj (proj32_1 sa) sb)) => [a oa av]. case:(oleT_el oa ox); first by move/q3=> xx;case:(oltNge sa); rewrite av. by rewrite av; move /oleSltP /q3. move: (q1 _ (OS_succ ox)) => [ua ub];apply: sc => //; apply /oleSltP. by apply: q4; apply: oltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)