Let x be given.
Assume Hx.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using recip_SNo_negcase x Hx H1 (from left to right).
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).
We will prove x < 0.
An exact proof term for the current goal is H1.
We prove the intermediate claim Lrmx: SNo (recip_SNo_pos (- x)).
An exact proof term for the current goal is SNo_recip_SNo_pos (- x) Lmx Lmxpos.
We prove the intermediate claim Lmrmx: SNo (- recip_SNo_pos (- x)).
An exact proof term for the current goal is SNo_minus_SNo (recip_SNo_pos (- x)) Lrmx.
We prove the intermediate claim L1: 0 < recip_SNo_pos (- x).
An exact proof term for the current goal is recip_SNo_pos_is_pos (- x) Lmx Lmxpos.
We prove the intermediate claim L2: - 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).
An exact proof term for the current goal is L1.
rewrite the current goal using recip_SNo_negcase (- (recip_SNo_pos (- x))) Lmrmx L2 (from left to right).
We will prove - recip_SNo_pos (- (- (recip_SNo_pos (- x)))) = x.
rewrite the current goal using minus_SNo_invol (recip_SNo_pos (- x)) Lrmx (from left to right).
rewrite the current goal using recip_SNo_pos_invol (- x) Lmx Lmxpos (from left to right).
An exact proof term for the current goal is minus_SNo_invol x Hx.
Assume H1: x = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using recip_SNo_0 (from left to right).
An exact proof term for the current goal is recip_SNo_0.
Assume H1: 0 < x.
rewrite the current goal using recip_SNo_poscase x H1 (from left to right).
rewrite the current goal using recip_SNo_poscase (recip_SNo_pos x) (recip_SNo_pos_is_pos x Hx H1) (from left to right).
An exact proof term for the current goal is recip_SNo_pos_invol x Hx H1.
∎