Let x be given.

Assume Hx Hxneg.

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 Lmxpos: 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.

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

Apply SNo_recip_SNo_pos to the current goal.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is Lmxpos.

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

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

Apply minus_SNo_Lt_contra1 0 (recip_SNo_pos (- x)) SNo_0 Lrmx 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_is_pos (- x) Lmx to the current goal.

We will prove 0 < - x.

An exact proof term for the current goal is Lmxpos.

∎