Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_SNo_com w (- z) Hw (SNo_minus_SNo z Hz) (from left to right).

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

An exact proof term for the current goal is add_SNo_minus_SNo_prop3 x y z w Hx Hy Hz Hw.

∎