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