Let x and y be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hxy: x ≤ y.

Apply SNoLeE x y Hx Hy Hxy to the current goal.

Assume H1: x < y.

We will prove - y ≤ - x.

Apply SNoLtLe to the current goal.

We will prove - y < - x.

An exact proof term for the current goal is minus_SNo_Lt_contra x y Hx Hy H1.

Assume H1: x = y.

We will prove - y ≤ - x.

rewrite the current goal using H1 (from left to right).

We will prove - y ≤ - y.

Apply SNoLe_ref to the current goal.

∎