Let x, y and z be given.
Assume Hx Hy Hz.
We will prove x * (y * z) = z * (x * y).
Use transitivity with x * (z * y), (x * z) * y, and (z * x) * y.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com y z Hy Hz.
An exact proof term for the current goal is mul_SNo_assoc x z y Hx Hz Hy.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com x z Hx Hz.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc z x y Hz Hx Hy.
∎