Let x, y and z be given.

Assume Hx Hy Hz.

Use transitivity with (x :/: y) * z, and (x * z) :/: y.

An exact proof term for the current goal is mul_SNo_com z (x :/: y) Hz (SNo_div_SNo x y Hx Hy).

An exact proof term for the current goal is mul_div_SNo_R x y z Hx Hy Hz.

Use f_equal.

An exact proof term for the current goal is mul_SNo_com x z Hx Hz.

∎