Let x be given.
Assume H1 H2 H3.
We prove the intermediate claim L1: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x H1.
Apply SNo_prereal_incr_lower_approx (- x) L1 (minus_SNo_prereal_1 x H1 H2) (minus_SNo_prereal_2 x H1 H3) to the current goal.
Let f be given.
Assume Hf.
Apply Hf to the current goal.
Assume Hf1: f ∈ SNoS_ ωω.
Assume Hf2: ∀n ∈ ω, f n < - x ∧ - x < f n + eps_ n ∧ ∀i ∈ n, f i < f n.
We prove the intermediate claim Lf: ∀n ∈ ω, SNo (f n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (f n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
Set g to be the term λn ∈ ω ⇒ - f n.
We use g to witness the existential quantifier.
Apply andI to the current goal.
We will prove g ∈ SNoS_ ωω.
We will prove (λn ∈ ω ⇒ - f n) ∈ ∏_ ∈ ω, SNoS_ ω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
We will prove - f n ∈ SNoS_ ω.
Apply minus_SNo_SNoS_omega to the current goal.
We will prove f n ∈ SNoS_ ω.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn.
Let n be given.
Assume Hn.
We will prove g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i.
We prove the intermediate claim L1: - f n + - eps_ n < x ∧ x < - f n ∧ ∀i ∈ n, - f n < g i.
Apply Hf2 n Hn to the current goal.
Assume H.
Apply H to the current goal.
Assume Hf2a: f n < - x.
Assume Hf2b: - x < f n + eps_ n.
Assume Hf2c: ∀i ∈ n, f i < f n.
Apply and3I to the current goal.
We will prove - f n + - eps_ n < x.
rewrite the current goal using minus_add_SNo_distr (f n) (eps_ n) (Lf n Hn) (SNo_eps_ n Hn) (from right to left).
We will prove - (f n + eps_ n) < x.
Apply minus_SNo_Lt_contra1 x (f n + eps_ n) H1 (SNo_add_SNo (f n) (eps_ n) (Lf n Hn) (SNo_eps_ n Hn)) to the current goal.
We will prove - x < f n + eps_ n.
An exact proof term for the current goal is Hf2b.
We will prove x < - f n.
Apply minus_SNo_Lt_contra2 (f n) x (Lf n Hn) H1 to the current goal.
We will prove f n < - x.
An exact proof term for the current goal is Hf2a.
Let i be given.
Assume Hi.
We prove the intermediate claim Li: i ∈ ω.
An exact proof term for the current goal is nat_p_omega i (nat_p_trans n (omega_nat_p n Hn) i Hi).
rewrite the current goal using beta ω (λn ⇒ - f n) i Li (from left to right).
We will prove - f n < - f i.
Apply minus_SNo_Lt_contra (f i) (f n) (Lf i Li) (Lf n Hn) to the current goal.
An exact proof term for the current goal is Hf2c i Hi.
We prove the intermediate claim L2: g n = - f n.
An exact proof term for the current goal is beta ω (λn ⇒ - f n) n Hn.
An exact proof term for the current goal is L2 (λu v ⇒ v + - eps_ n < x ∧ x < v ∧ ∀i ∈ n, v < g i) L1.
∎