Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_com z w Hz Hw (from left to right).
We will
prove (x + y) + (w + z) = (x + w) + (y + z).
An exact proof term for the current goal is add_SNo_com_4_inner_mid x y w z Hx Hy Hw Hz.
∎