proposition: Lemma Gamma0_s x y: x <o Gamma_0 -> y <o Gamma_0 -> Sphi x y <o Gamma_0.
proof: Proof. move => sa sb. have [sc sd]:= Gamma0_p. have ox := (proj31_1 sa). have oy:= (proj31_1 sb). have og :=(proj32_1 sb). rewrite - sc. apply/(Sphi_p7 oy OS0 ox og); split. + by rewrite sc. + by move: (proj2 sa). + by move => [/(oltNge sa)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)