Let x, y, z and w be given.

Assume Hx Hy Hz Hw H1.

We will prove x + y + - z ≤ w.

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

We will prove (x + y) + - z ≤ w.

Apply add_SNo_minus_Le1b (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw to the current goal.

An exact proof term for the current goal is H1.

∎