proposition: Lemma first_derivation_p1 f: normal_ofs f -> (first_derivation f \0o) = the_least_fixedpoint_ge f \0o.
proof: Proof. move => nf; move:(iclosed_fixpoints nf) => [pa pb]. set p := (fun z => 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 OS0) => [sa sb sc]. apply: oleA. by move: (q2 _ (conj (proj32 sa) sb)) => [a /ole0x aa ->]; apply: q3. by move: (q1 _ OS0) => [ /ole0x ha hb]; apply: sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)