proposition: Lemma OS_Sphi x y: ordinalp x -> ordinalp y -> ordinalp (Sphi x y).
proof: Proof. move: (all_der_pow_aux) => [ha hb] ox oy. exact: (OS_all_der ha hb oy ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)