Let x be given.
Assume Hx.
Let p be given.
Assume Hp.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 _ _ Hx4 Hx5.
Let f be given.
Assume Hf.
Apply Hf to the current goal.
Assume Hf1 Hf2.
Let g be given.
Assume Hg.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We prove the intermediate
claim Lf:
∀n ∈ ω, SNo (f n).
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lg:
∀n ∈ ω, SNo (g n).
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lf1:
∀n ∈ ω, f n < x.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lf2:
∀n ∈ ω, x < f n + eps_ n.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lf3:
∀n ∈ ω, ∀i ∈ n, f i < f n.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lg1:
∀n ∈ ω, g n + - eps_ n < x.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lg2:
∀n ∈ ω, x < g n.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lg3:
∀n ∈ ω, ∀i ∈ n, g n < g i.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lfg:
∀n m ∈ ω, f n < g m.
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
Apply SNoLt_tra (f n) x (g m) (Lf n Hn) Hx1 (Lg m Hm) to the current goal.
An exact proof term for the current goal is Lf1 n Hn.
An exact proof term for the current goal is Lg2 m Hm.
Set L to be the term
{f n|n ∈ ω}.
Set R to be the term
{g n|n ∈ ω}.
We prove the intermediate
claim Lxfg:
x = SNoCut L R.
rewrite the current goal using
SNo_eta x Hx1 (from left to right).
Let w be given.
Apply SNoL_E x Hx1 w Hw to the current goal.
We prove the intermediate
claim Lw1:
w ∈ SNoS_ ω.
We prove the intermediate
claim Lw2:
0 < x + - w.
An
exact proof term for the current goal is
SNoLt_minus_pos w x Hw1 Hx1 Hw3.
We prove the intermediate
claim Lw3:
∃k ∈ ω, w + eps_ k ≤ x.
Apply dneg to the current goal.
We prove the intermediate
claim Lw3a:
w = x.
Apply Hx4 w Lw1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (x + - w) Lw2 (from left to right).
An exact proof term for the current goal is H8.
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
rewrite the current goal using Lw3a (from right to left) at position 1.
An exact proof term for the current goal is Hw3.
Apply Lw3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Apply SNoLt_tra w (f k) (SNoCut L R) Hw1 (Lf k Hk1) H2 to the current goal.
We will
prove x < f k + eps_ k.
Apply Hf2 k Hk1 to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
An exact proof term for the current goal is H5 k Hk1.
Let z be given.
Apply SNoR_E x Hx1 z Hz to the current goal.
We prove the intermediate
claim Lz1:
z ∈ SNoS_ ω.
We prove the intermediate
claim Lz2:
0 < z + - x.
An
exact proof term for the current goal is
SNoLt_minus_pos x z Hx1 Hz1 Hz3.
We prove the intermediate
claim Lz3:
∃k ∈ ω, x + eps_ k ≤ z.
Apply dneg to the current goal.
We prove the intermediate
claim Lz3a:
z = x.
Apply Hx4 z Lz1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (z + - x) Lz2 (from left to right).
An exact proof term for the current goal is H8.
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
rewrite the current goal using Lz3a (from right to left) at position 2.
An exact proof term for the current goal is Hz3.
Apply Lz3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Apply SNoLt_tra (SNoCut L R) (g k) z H2 (Lg k Hk1) Hz1 to the current goal.
An exact proof term for the current goal is H6 k Hk1.
We will
prove g k < x + eps_ k.
An exact proof term for the current goal is Lg1 k Hk1.
An exact proof term for the current goal is Hk2.
Let w be given.
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
Let n be given.
Assume Hn.
rewrite the current goal using Hwn (from left to right).
An exact proof term for the current goal is Lf1 n Hn.
Let z be given.
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
Let m be given.
Assume Hm.
rewrite the current goal using Hzm (from left to right).
An exact proof term for the current goal is Lg2 m Hm.
An exact proof term for the current goal is Hp f Hf1 g Hg1 Lf1 Lf2 Lf3 Lg1 Lg2 Lg3 H1 Lxfg.
∎