proposition: Lemma Spsi_p11 x y : ordinalp x -> ordinalp y -> Spsi x y <=o Sphi x (osucc y).
proof: Proof. move => ox oy;rewrite /Spsi; Ytac h3. apply: oleR; apply:OS_Sphi; fprops. by move:((proj1 (Sphi_p1 ox) _ _ (oltS oy))) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)