Let x be given.

Assume Hx H1.

Let q be given.

Assume Hq1: q ∈ SNoS_ ω.

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

Assume Hq2: ∀k ∈ ω, abs_SNo (q + x) < eps_ k.

We will prove q = - x.

Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.

Assume Hq1a Hq1b Hq1c Hq1d.

rewrite the current goal using minus_SNo_invol q Hq1c (from right to left).

We will prove - - q = - x.

Use f_equal.

We will prove - q = x.

Apply H1 (- q) (minus_SNo_SNoS_omega q Hq1) to the current goal.

Let k be given.

Assume Hk.

We will prove abs_SNo (- q + - x) < eps_ k.

rewrite the current goal using abs_SNo_dist_swap (- q) x (SNo_minus_SNo q Hq1c) Hx (from left to right).

We will prove abs_SNo (x + - - q) < eps_ k.

rewrite the current goal using minus_SNo_invol q Hq1c (from left to right).

We will prove abs_SNo (x + q) < eps_ k.

rewrite the current goal using add_SNo_com x q Hx Hq1c (from left to right).

We will prove abs_SNo (q + x) < eps_ k.

An exact proof term for the current goal is Hq2 k Hk.

∎