Assume H1: x < 0.

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

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).

We will prove x < 0.

An exact proof term for the current goal is H1.

We will prove x * (- recip_SNo_pos (- x)) = 1.

rewrite the current goal using mul_SNo_minus_distrR x (recip_SNo_pos (- x)) Hx (SNo_recip_SNo_pos (- x) (SNo_minus_SNo x Hx) L1) (from left to right).

We will prove - (x * recip_SNo_pos (- x)) = 1.

rewrite the current goal using mul_SNo_minus_distrL x (recip_SNo_pos (- x)) Hx (SNo_recip_SNo_pos (- x) (SNo_minus_SNo x Hx) L1) (from right to left).

We will prove (- x) * recip_SNo_pos (- x) = 1.

An exact proof term for the current goal is recip_SNo_pos_invR (- x) (SNo_minus_SNo x Hx) L1.

Assume H1: x = 0.

We will prove False.

An exact proof term for the current goal is Hx0 H1.

Assume H1: 0 < x.

rewrite the current goal using recip_SNo_poscase x H1 (from left to right).

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