Let x be given.

Assume Hx.

An exact proof term for the current goal is mul_SNo_zeroL (recip_SNo x) (SNo_recip_SNo x Hx).

∎