Let z be given.

Assume Hz.

Let w be given.

Assume Hw.

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

∎