Let x, y, z, w and v be given.

Assume Hx Hy Hz Hw Hv.

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

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

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

∎