Let z be given.

Assume Hz Hznz.

rewrite the current goal using mul_CSNo_com (recip_CSNo z) z (CSNo_recip_CSNo z Hz) Hz (from left to right).

An exact proof term for the current goal is recip_CSNo_invR z Hz Hznz.

∎