Let x be given.

Assume Hx1 Hx2.

Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal x Hx1 to the current goal.

Assume Hx1a Hx1b Hx1c Hx1d.

We prove the intermediate claim Lx1: - x ∈ SNoS_ (ordsucc ω).

An exact proof term for the current goal is minus_SNo_SNoS_ (ordsucc ω) ordsucc_omega_ordinal x Hx1.

We prove the intermediate claim Lx2: - x < ω.

Apply minus_SNo_Lt_contra1 ω x SNo_omega Hx1c to the current goal.

We will prove - ω < x.

An exact proof term for the current goal is Hx2.

Apply SNoS_ordsucc_omega_bdd_above (- x) Lx1 Lx2 to the current goal.

Let N be given.

Assume HN.

Apply HN to the current goal.

Assume HN1: N ∈ ω.

Assume HN2: - x < N.

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HN1.

We will prove - N < x.

Apply minus_SNo_Lt_contra1 x N Hx1c (omega_SNo N HN1) to the current goal.

We will prove - x < N.

An exact proof term for the current goal is HN2.

∎