proposition: Lemma Sphi_p5 : normal_ofs (Sphi ^~ \0o).
proof: Proof. move: (all_der_pow_aux) => [ha hb]. have hc: omega0 ^o \0o <> \0o by apply: oopow_nz; fprops. exact:(all_der_p13 ha hb hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)