proposition: Lemma first_derivation_p f (fp := first_derivation f): normal_ofs f -> ( (forall x, ordinalp x -> f (fp x) = fp x) /\ (forall y, ordinalp y -> f y = y -> exists2 x, ordinalp x & y = fp x)).
proof: Proof. move => pa. move:(iclosed_fixpoints pa). pose p z :=(ordinalp z /\ f z = z). have sa: (forall x, p x -> ordinalp x) by move => x []. rewrite /fp /first_derivation -/p. move => [sc sd]. move:(ordinals_col_p1 sa sd) => [pb pc pd pe [pf pg]]. by split; [move => x /pb [_] | move => y oy fy; apply:pc ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)