Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_HSNo_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_HSNo_com_4_inner_mid x y w z Hx Hy Hw Hz.

∎