Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using mul_div_SNo_L z w (x :/: y) Hz Hw (SNo_div_SNo x y Hx Hy) (from left to right).

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

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

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

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

∎