Let x, y and z be given.

Assume Hx Hy Hz H1.

Apply add_SNo_Lt1_cancel x (- y) (z + y) Hx (SNo_minus_SNo y Hy) (SNo_add_SNo z y Hz Hy) to the current goal.

We will prove x + - y < (z + y) + - y.

rewrite the current goal using add_SNo_assoc z y (- y) Hz Hy (SNo_minus_SNo y Hy) (from right to left).

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

rewrite the current goal using add_SNo_0R z Hz (from left to right).

An exact proof term for the current goal is H1.

∎