Let x, y and z be given.
Assume Hx Hy Hz.
Apply xm (y = 0) to the current goal.
Assume H1: y = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
rewrite the current goal using div_SNo_0_denum (x * z) (SNo_mul_SNo x z Hx Hz) (from left to right).
We will prove 0 * z = 0.
An exact proof term for the current goal is mul_SNo_zeroL z Hz.
Assume H1: y ≠ 0.
Apply mul_SNo_nonzero_cancel y ((x :/: y) * z) ((x * z) :/: y) Hy H1 (SNo_mul_SNo (x :/: y) z (SNo_div_SNo x y Hx Hy) Hz) (SNo_div_SNo (x * z) y (SNo_mul_SNo x z Hx Hz) Hy) to the current goal.
We will prove y * (x :/: y) * z = y * (x * z) :/: y.
rewrite the current goal using mul_div_SNo_invR (x * z) y (SNo_mul_SNo x z Hx Hz) Hy H1 (from left to right).
We will prove y * (x :/: y) * z = x * z.
rewrite the current goal using mul_SNo_assoc y (x :/: y) z Hy (SNo_div_SNo x y Hx Hy) Hz (from left to right).
We will prove (y * (x :/: y)) * z = x * z.
Use f_equal.
We will prove y * (x :/: y) = x.
An exact proof term for the current goal is mul_div_SNo_invR x y Hx Hy H1.
∎