proposition: Lemma Sphi_p2 x: ordinalp x -> first_derivation (Sphi x) =1o (Sphi (osucc x)).
proof: Proof. move: (all_der_pow_aux) => [ha hb]. move => ox; exact: (all_der_p14 ha hb ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)