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.
An exact proof term for the current goal is H1.
∎