Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_SNo_rotate_3_1 y z w Hy Hz Hw (from left to right).

We will prove x + w + y + z = w + x + y + z.

An exact proof term for the current goal is add_SNo_com_3_0_1 x w (y + z) Hx Hw (SNo_add_SNo y z Hy Hz).

∎