Let x, y and z be given.

Assume Hx Hy Hz H1.

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

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

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

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

rewrite the current goal using add_SNo_0R x Hx (from left to right).

An exact proof term for the current goal is H1.

∎