proposition: Lemma Sphi_p7 x y i j: ordinalp x -> ordinalp y -> ordinalp i -> ordinalp j -> (Sphi i x <o Sphi j y <-> [/\ i <o j -> x <o Sphi j y, i = j -> x <o y & j <o i -> Sphi i x <o y]).
proof: Proof. move: (all_der_pow_aux) => [ha hb] ox oy oi oj. exact: (all_der_p10 ha hb ox oy oi oj ). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)