Let z and w be given.

Assume Hz Hw Hw0.

rewrite the current goal using mul_CSNo_com w (div_CSNo z w) Hw (CSNo_div_CSNo z w Hz Hw) (from left to right).

An exact proof term for the current goal is mul_div_CSNo_invL z w Hz Hw Hw0.

∎