Let x be given.

Assume Hx Hxpos.

Apply recip_SNo_pos_prop1 x Hx Hxpos to the current goal.

Assume _ H.

An exact proof term for the current goal is H.

∎