Let x and y be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hxy: x < - y.

We will prove y < - x.

rewrite the current goal using minus_SNo_invol y Hy (from right to left).

We will prove - - y < - x.

Apply minus_SNo_Lt_contra x (- y) Hx (SNo_minus_SNo y Hy) to the current goal.

We will prove x < - y.

An exact proof term for the current goal is Hxy.

∎