Let x, y and z be given.

Assume Hx Hy Hz H1.

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

We will prove (x + - y) + y ≤ z + 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.

∎