proposition: Lemma first_derivation_p2 f: normal_ofs f -> f \0o <> \0o -> (first_derivation f \0o) = the_least_fixedpoint_ge f \1o.
proof: Proof. move => nf nf0; move:(iclosed_fixpoints nf) => [pa pb]. set p := (fun z : Set => ordinalp z /\ f z = z). have pc: forall x, p x -> ordinalp x by move=> x []. move: (ordinals_col_p1 pc pb) => [q1 q2 q3 q4 [q5 q6]]. rewrite /first_derivation -/p. move: (normal_ofs_fix nf OS1) => [sa sb sc]. apply: oleA. by move: (q2 _ (conj (proj32 sa) sb)) => [a /ole0x oa ->]; apply: q3. move: (q1 _ OS0) => [ ha hb]; apply: sc => //;apply: oge1 => //. by move => ba; case: nf0; rewrite - ba. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)