Let x be given.
Assume Hx.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is real_SNo x Hx.
Apply SNoLt_trichotomy_or_impred x 0 Lx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using recip_SNo_negcase x Lx H1 (from left to right).
We will prove - recip_SNo_pos (- x) ∈ real.
Apply real_minus_SNo (recip_SNo_pos (- x)) to the current goal.
We will prove recip_SNo_pos (- x) ∈ real.
Apply real_recip_SNo_pos (- x) to the current goal.
We will prove - x ∈ real.
An exact proof term for the current goal is real_minus_SNo x Hx.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Lx 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 H1.
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).
We will prove 0 ∈ real.
An exact proof term for the current goal is real_0.
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 real_recip_SNo_pos x Hx H1.
∎