Let x, y and z be given.

Assume Hx Hy Hz H1.

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

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

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

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

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.

∎