Let x be given.

Assume Hx Hxpos.

Apply real_recip_SNo_lem1 x (real_SNo x Hx) Hx Hxpos to the current goal.

Assume H _.

An exact proof term for the current goal is H.

∎