Let z and w be given.

Assume Hz Hw Hw0.

We will prove (z ⨯ recip_CSNo w) ⨯ w = z.

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

We will prove z ⨯ (recip_CSNo w ⨯ w) = z.

rewrite the current goal using recip_CSNo_invL w Hw Hw0 (from left to right).

We will prove z ⨯ 1 = z.

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

∎