Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Let fL be given.
Assume HfL.
Let fR be given.
Assume HfR HfL1 HfL2 HfL3 HfR1 HfR2 HfR3 HfLR HxfLR.
Let gL be given.
Assume HgL.
Let gR be given.
Assume HgR HgL1 HgL2 HgL3 HgR1 HgR2 HgR3 HgLR HygLR.
Set L to be the term
{hL n|n ∈ ω}.
Set R to be the term
{hR n|n ∈ ω}.
We prove the intermediate
claim Lx:
SNo x.
An
exact proof term for the current goal is
real_SNo x Hx.
We prove the intermediate
claim Ly:
SNo y.
An
exact proof term for the current goal is
real_SNo y Hy.
We prove the intermediate
claim Lxy:
SNo (x + y).
An
exact proof term for the current goal is
SNo_add_SNo x y Lx Ly.
Let n be given.
Assume Hn.
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
Let n be given.
Assume Hn.
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
Let n be given.
Assume Hn.
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
Let n be given.
Assume Hn.
Let n be given.
Assume Hn.
Assume _ _ H _.
An exact proof term for the current goal is H.
Let n be given.
Assume Hn.
Let n be given.
Assume Hn.
We prove the intermediate
claim LhLb:
∀n ∈ ω, SNo (hL n).
Let n be given.
Assume Hn.
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim LhRb:
∀n ∈ ω, SNo (hR n).
Let n be given.
Assume Hn.
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L1:
hL ∈ SNoS_ ωω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
An exact proof term for the current goal is LfLa n Hn.
An exact proof term for the current goal is LgLa n Hn.
We prove the intermediate
claim L2:
hR ∈ SNoS_ ωω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
An exact proof term for the current goal is LfRa n Hn.
An exact proof term for the current goal is LgRa n Hn.
We prove the intermediate
claim L3:
∀n ∈ ω, hL n < x + y.
Let n be given.
Assume Hn.
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim L4:
∀n ∈ ω, x + y < hL n + eps_ n.
Let n be given.
Assume Hn.
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim L5:
∀n ∈ ω, ∀i ∈ n, hL i < hL n.
Let n be given.
Assume Hn.
Let i be given.
Assume Hi.
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim Li:
i ∈ ω.
rewrite the current goal using LhL i Li (from left to right).
We prove the intermediate
claim L6:
∀n ∈ ω, hR n + - eps_ n < x + y.
Let n be given.
Assume Hn.
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L7:
∀n ∈ ω, x + y < hR n.
Let n be given.
Assume Hn.
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L8:
∀n ∈ ω, ∀i ∈ n, hR n < hR i.
Let n be given.
Assume Hn.
Let i be given.
Assume Hi.
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim Li:
i ∈ ω.
rewrite the current goal using LhR i Li (from left to right).
We prove the intermediate
claim LLR:
SNoCutP L R.
Apply and3I to the current goal.
Let w be given.
Assume Hw.
Let n be given.
rewrite the current goal using Hwn (from left to right).
We will
prove SNo (hL n).
An exact proof term for the current goal is LhLb n Hn.
Let z be given.
Assume Hz.
Let m be given.
rewrite the current goal using Hzm (from left to right).
We will
prove SNo (hR m).
An exact proof term for the current goal is LhRb m Hm.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Let n be given.
rewrite the current goal using Hwn (from left to right).
Let m be given.
rewrite the current goal using Hzm (from left to right).
We will
prove hL n < hR m.
Apply SNoLt_tra (hL n) (x + y) (hR m) (LhLb n Hn) (SNo_add_SNo x y Lx Ly) (LhRb m Hm) to the current goal.
We will
prove hL n < x + y.
An exact proof term for the current goal is L3 n Hn.
We will
prove x + y < hR m.
An exact proof term for the current goal is L7 m Hm.
Assume HLR1 HLR2 HLR3 HLR4 HLR5.
We prove the intermediate
claim L9:
x + y = SNoCut L R.
rewrite the current goal using
add_SNo_eq x Lx y Ly (from left to right).
Let w be given.
Assume Hw.
Let w' be given.
Assume Hww'.
rewrite the current goal using Hww' (from left to right).
Apply SNoL_E x Lx w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3.
We prove the intermediate
claim Lw'1:
w' ∈ SNoS_ ω.
We prove the intermediate
claim Lw'2:
∃n ∈ ω, w' + y ≤ hL n.
Apply dneg to the current goal.
We prove the intermediate
claim Lw'2a:
0 < x + - w'.
We prove the intermediate
claim Lw'2b:
w' = x.
Apply Lx2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk.
rewrite the current goal using
pos_abs_SNo (x + - w') Lw'2a (from left to right).
We will
prove x < eps_ k + w'.
Assume H2.
An exact proof term for the current goal is H2.
Apply HC 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.
We will
prove w' + y ≤ hL k.
We will
prove w' + y < hL k.
We will
prove (w' + y) + eps_ k ≤ x + y.
We will
prove (w' + eps_ k) + y ≤ x + y.
We will
prove w' + eps_ k ≤ x.
We will
prove eps_ k + w' ≤ x.
An exact proof term for the current goal is H2.
We will
prove x + y < hL k + eps_ k.
An exact proof term for the current goal is L4 k Hk.
rewrite the current goal using Lw'2b (from right to left) at position 1.
An exact proof term for the current goal is Hw'3.
Apply Lw'2 to the current goal.
Let n be given.
Assume Hn.
Apply Hn to the current goal.
Assume Hn1 Hn2.
We will
prove w' + y ≤ hL n.
An exact proof term for the current goal is Hn2.
Apply HLR3 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
Let w' be given.
Assume Hww'.
rewrite the current goal using Hww' (from left to right).
Apply SNoL_E y Ly w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3.
We prove the intermediate
claim Lw'1:
w' ∈ SNoS_ ω.
We prove the intermediate
claim Lw'2:
∃n ∈ ω, x + w' ≤ hL n.
Apply dneg to the current goal.
We prove the intermediate
claim Lw'2a:
0 < y + - w'.
We prove the intermediate
claim Lw'2b:
w' = y.
Apply Ly2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk.
rewrite the current goal using
pos_abs_SNo (y + - w') Lw'2a (from left to right).
We will
prove y < eps_ k + w'.
Assume H2.
An exact proof term for the current goal is H2.
Apply HC 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.
We will
prove x + w' ≤ hL k.
We will
prove x + w' < hL k.
We will
prove (x + w') + eps_ k ≤ x + y.
We will
prove x + (w' + eps_ k) ≤ x + y.
We will
prove w' + eps_ k ≤ y.
We will
prove eps_ k + w' ≤ y.
An exact proof term for the current goal is H2.
We will
prove x + y < hL k + eps_ k.
An exact proof term for the current goal is L4 k Hk.
rewrite the current goal using Lw'2b (from right to left) at position 1.
An exact proof term for the current goal is Hw'3.
Apply Lw'2 to the current goal.
Let n be given.
Assume Hn.
Apply Hn to the current goal.
Assume Hn1 Hn2.
We will
prove x + w' ≤ hL n.
An exact proof term for the current goal is Hn2.
Apply HLR3 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
Let z be given.
Assume Hz.
Let z' be given.
Assume Hzz'.
rewrite the current goal using Hzz' (from left to right).
Apply SNoR_E x Lx z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3.
We prove the intermediate
claim Lz'1:
z' ∈ SNoS_ ω.
We prove the intermediate
claim Lz'2:
∃n ∈ ω, hR n ≤ z' + y.
Apply dneg to the current goal.
We prove the intermediate
claim Lz'2a:
0 < z' + - x.
We prove the intermediate
claim Lz'2b:
z' = x.
Apply Lx2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk.
rewrite the current goal using
pos_abs_SNo (z' + - x) Lz'2a (from left to right).
We will
prove z' < eps_ k + x.
Assume H2.
An exact proof term for the current goal is H2.
Apply HC 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.
We will
prove hR k ≤ z' + y.
An exact proof term for the current goal is L6 k Hk.
We will
prove (x + y) + eps_ k ≤ z' + y.
We will
prove (x + eps_ k) + y ≤ z' + y.
We will
prove x + eps_ k ≤ z'.
An exact proof term for the current goal is H2.
rewrite the current goal using Lz'2b (from right to left) at position 2.
An exact proof term for the current goal is Hz'3.
Apply Lz'2 to the current goal.
Let n be given.
Assume Hn.
Apply Hn to the current goal.
Assume Hn1 Hn2.
Apply HLR4 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
We will
prove hR n ≤ z' + y.
An exact proof term for the current goal is Hn2.
Let z' be given.
Assume Hzz'.
rewrite the current goal using Hzz' (from left to right).
Apply SNoR_E y Ly z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3.
We prove the intermediate
claim Lz'1:
z' ∈ SNoS_ ω.
We prove the intermediate
claim Lz'2:
∃n ∈ ω, hR n ≤ x + z'.
Apply dneg to the current goal.
We prove the intermediate
claim Lz'2a:
0 < z' + - y.
We prove the intermediate
claim Lz'2b:
z' = y.
Apply Ly2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk.
rewrite the current goal using
pos_abs_SNo (z' + - y) Lz'2a (from left to right).
We will
prove z' < eps_ k + y.
Assume H2.
An exact proof term for the current goal is H2.
Apply HC 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.
We will
prove hR k ≤ x + z'.
An exact proof term for the current goal is L6 k Hk.
We will
prove (x + y) + eps_ k ≤ x + z'.
We will
prove x + (y + eps_ k) ≤ x + z'.
We will
prove y + eps_ k ≤ z'.
An exact proof term for the current goal is H2.
rewrite the current goal using Lz'2b (from right to left) at position 2.
An exact proof term for the current goal is Hz'3.
Apply Lz'2 to the current goal.
Let n be given.
Assume Hn.
Apply Hn to the current goal.
Assume Hn1 Hn2.
Apply HLR4 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
We will
prove hR n ≤ x + z'.
An exact proof term for the current goal is Hn2.
Let w be given.
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
Let n be given.
rewrite the current goal using Hwn (from left to right).
We will
prove hL n < x + y.
An exact proof term for the current goal is L3 n Hn.
Let z be given.
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
Let n be given.
rewrite the current goal using Hzn (from left to right).
We will
prove x + y < hR n.
An exact proof term for the current goal is L7 n Hn.
∎