Let x be given.

Assume Hx Hxneg.

rewrite the current goal using recip_SNo_negcase x Hx Hxneg (from left to right).

We will prove - recip_SNo_pos (- x) < 0.

We prove the intermediate claim Lmx: SNo (- x).

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

We prove the intermediate claim L1: 0 < - x.

Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.

We will prove x < - 0.

rewrite the current goal using minus_SNo_0 (from left to right).

An exact proof term for the current goal is Hxneg.

Apply minus_SNo_Lt_contra1 0 (recip_SNo_pos (- x)) SNo_0 (SNo_recip_SNo_pos (- x) Lmx L1) to the current goal.

We will prove - 0 < recip_SNo_pos (- x).

rewrite the current goal using minus_SNo_0 (from left to right).

We will prove 0 < recip_SNo_pos (- x).

Apply recip_SNo_pos_pos (- x) (SNo_minus_SNo x Hx) to the current goal.

We will prove 0 < - x.

An exact proof term for the current goal is L1.

∎