Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_assoc x y z Hx Hy Hz (from left to right).
We will prove ((x + y) + z) + (- z + w) = x + y + w.
rewrite the current goal using add_SNo_assoc (x + y) z (- z + w) (SNo_add_SNo x y Hx Hy) Hz (SNo_add_SNo (- z) w (SNo_minus_SNo z Hz) Hw) (from right to left).
We will prove (x + y) + (z + - z + w) = x + y + w.
rewrite the current goal using add_SNo_minus_L2' z w Hz Hw (from left to right).
We will prove (x + y) + w = x + y + w.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y w Hx Hy Hw.
∎