Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using mul_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 mul_SNo_com_3_0_1 x w (y * z) Hx Hw (SNo_mul_SNo y z Hy Hz).

∎