Let x be given.

Assume Hx Hx0.

rewrite the current goal using mul_SNo_com (recip_SNo x) x (SNo_recip_SNo x Hx) Hx (from left to right).

We will prove x * recip_SNo x = 1.

An exact proof term for the current goal is recip_SNo_invR x Hx Hx0.

∎