Let x be given.
Assume Hx.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7.
Apply real_I to the current goal.
We will prove - x ∈ SNoS_ (ordsucc ω).
An exact proof term for the current goal is minus_SNo_SNoS_ (ordsucc ω) ordsucc_omega_ordinal x Hx3.
We will prove - x ≠ ω.
Assume H1: - x = ω.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
rewrite the current goal using minus_SNo_invol x Hx1 (from right to left) at position 1.
We will prove - - x < x.
rewrite the current goal using H1 (from left to right).
We will prove - ω < x.
An exact proof term for the current goal is Hx4.
We will prove - x ≠ - ω.
Assume H1: - x = - ω.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
rewrite the current goal using minus_SNo_invol x Hx1 (from right to left) at position 2.
We will prove x < - - x.
rewrite the current goal using H1 (from left to right).
We will prove x < - - ω.
rewrite the current goal using minus_SNo_invol ω SNo_omega (from left to right).
We will prove x < ω.
An exact proof term for the current goal is Hx5.
We will prove ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x.
An exact proof term for the current goal is minus_SNo_prereal_1 x Hx1 Hx6.
∎