Let z and w be given.

Assume Hz Hw.

An exact proof term for the current goal is CSNo_mul_CSNo z (recip_CSNo w) Hz (CSNo_recip_CSNo w Hw).

∎