proposition: Lemma Sphi_p4 y j: ordinalp y -> \0o <o j -> (forall i, i <o j -> Sphi i y = y) -> (exists2 x, ordinalp x & y = Sphi j x).
proof: Proof. move: (all_der_pow_aux) => [ha hb] oy jp h. exact:(all_der_p8 ha hb oy jp h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)