Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using mul_SNo_assoc (x * y) z w (SNo_mul_SNo x y Hx Hy) Hz Hw (from left to right).

We will prove ((x * y) * z) * w = (x * z) * (y * w).

rewrite the current goal using mul_SNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).

We will prove ((x * z) * y) * w = (x * z) * (y * w).

Use symmetry.

An exact proof term for the current goal is mul_SNo_assoc (x * z) y w (SNo_mul_SNo x z Hx Hz) Hy Hw.

∎