Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply SNo_approx_real_rep x Hx to the current goal.
Let fL be given.
Assume HfL.
Let fR be given.
Assume HfR HfL1 HfL2 HfL3 HfR1 HfR2 HfR3 HfLR HxfLR.
Apply SNo_approx_real_rep y Hy to the current goal.
Let gL be given.
Assume HgL.
Let gR be given.
Assume HgR HgL1 HgL2 HgL3 HgR1 HgR2 HgR3 HgLR HygLR.
Set hL to be the term λn ∈ ω ⇒ fL (ordsucc n) + gL (ordsucc n).
Set hR to be the term λn ∈ ω ⇒ fR (ordsucc n) + gR (ordsucc n).
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.
We prove the intermediate claim Lx2: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
An exact proof term for the current goal is real_SNoS_omega_prop x Hx.
We prove the intermediate claim Ly2: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - y) < eps_ k) → q = y.
An exact proof term for the current goal is real_SNoS_omega_prop y Hy.
We prove the intermediate claim LfLa: ∀n ∈ ω, fL (ordsucc n) ∈ SNoS_ ω.
Let n be given.
Assume Hn.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) fL (ordsucc n) HfL (omega_ordsucc n Hn).
We prove the intermediate claim LfLb: ∀n ∈ ω, SNo (fL (ordsucc n)).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (fL (ordsucc n)) (LfLa n Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LgLa: ∀n ∈ ω, gL (ordsucc n) ∈ SNoS_ ω.
Let n be given.
Assume Hn.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) gL (ordsucc n) HgL (omega_ordsucc n Hn).
We prove the intermediate claim LgLb: ∀n ∈ ω, SNo (gL (ordsucc n)).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (gL (ordsucc n)) (LgLa n Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LfRa: ∀n ∈ ω, fR (ordsucc n) ∈ SNoS_ ω.
Let n be given.
Assume Hn.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) fR (ordsucc n) HfR (omega_ordsucc n Hn).
We prove the intermediate claim LfRb: ∀n ∈ ω, SNo (fR (ordsucc n)).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (fR (ordsucc n)) (LfRa n Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LgRa: ∀n ∈ ω, gR (ordsucc n) ∈ SNoS_ ω.
Let n be given.
Assume Hn.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) gR (ordsucc n) HgR (omega_ordsucc n Hn).
We prove the intermediate claim LgRb: ∀n ∈ ω, SNo (gR (ordsucc n)).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (gR (ordsucc n)) (LgRa n Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LhL: ∀n ∈ ω, hL n = fL (ordsucc n) + gL (ordsucc n).
Let n be given.
Assume Hn.
An exact proof term for the current goal is beta ω (λn ⇒ fL (ordsucc n) + gL (ordsucc n)) n Hn.
We prove the intermediate claim LhR: ∀n ∈ ω, hR n = fR (ordsucc n) + gR (ordsucc n).
Let n be given.
Assume Hn.
An exact proof term for the current goal is beta ω (λn ⇒ fR (ordsucc n) + gR (ordsucc n)) n 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 will prove SNo (fL (ordsucc n) + gL (ordsucc n)).
An exact proof term for the current goal is SNo_add_SNo (fL (ordsucc n)) (gL (ordsucc n)) (LfLb n Hn) (LgLb n Hn).
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 will prove SNo (fR (ordsucc n) + gR (ordsucc n)).
An exact proof term for the current goal is SNo_add_SNo (fR (ordsucc n)) (gR (ordsucc n)) (LfRb n Hn) (LgRb n Hn).
We prove the intermediate claim L1: hL ∈ SNoS_ ωω.
We will prove (λn ∈ ω ⇒ fL (ordsucc n) + gL (ordsucc n)) ∈ ∏_ ∈ ω, SNoS_ ω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
We will prove fL (ordsucc n) + gL (ordsucc n) ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
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_ ωω.
We will prove (λn ∈ ω ⇒ fR (ordsucc n) + gR (ordsucc n)) ∈ ∏_ ∈ ω, SNoS_ ω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
We will prove fR (ordsucc n) + gR (ordsucc n) ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
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 will prove fL (ordsucc n) + gL (ordsucc n) < x + y.
Apply add_SNo_Lt3 (fL (ordsucc n)) (gL (ordsucc n)) x y (LfLb n Hn) (LgLb n Hn) Lx Ly to the current goal.
We will prove fL (ordsucc n) < x.
An exact proof term for the current goal is HfL1 (ordsucc n) (omega_ordsucc n Hn).
We will prove gL (ordsucc n) < y.
An exact proof term for the current goal is HgL1 (ordsucc n) (omega_ordsucc n Hn).
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 will prove x + y < (fL (ordsucc n) + gL (ordsucc n)) + eps_ n.
rewrite the current goal using eps_ordsucc_half_add n (omega_nat_p n Hn) (from right to left).
We will prove x + y < (fL (ordsucc n) + gL (ordsucc n)) + (eps_ (ordsucc n) + eps_ (ordsucc n)).
We prove the intermediate claim LeSn: SNo (eps_ (ordsucc n)).
An exact proof term for the current goal is SNo_eps_ (ordsucc n) (omega_ordsucc n Hn).
rewrite the current goal using add_SNo_com_4_inner_mid (fL (ordsucc n)) (gL (ordsucc n)) (eps_ (ordsucc n)) (eps_ (ordsucc n)) (LfLb n Hn) (LgLb n Hn) LeSn LeSn (from left to right).
We will prove x + y < (fL (ordsucc n) + eps_ (ordsucc n)) + (gL (ordsucc n) + eps_ (ordsucc n)).
Apply add_SNo_Lt3 x y (fL (ordsucc n) + eps_ (ordsucc n)) (gL (ordsucc n) + eps_ (ordsucc n)) Lx Ly (SNo_add_SNo (fL (ordsucc n)) (eps_ (ordsucc n)) (LfLb n Hn) LeSn) (SNo_add_SNo (gL (ordsucc n)) (eps_ (ordsucc n)) (LgLb n Hn) LeSn) to the current goal.
An exact proof term for the current goal is HfL2 (ordsucc n) (omega_ordsucc n Hn).
An exact proof term for the current goal is HgL2 (ordsucc n) (omega_ordsucc n Hn).
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 ∈ ω.
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 LhL i Li (from left to right).
We will prove fL (ordsucc i) + gL (ordsucc i) < fL (ordsucc n) + gL (ordsucc n).
Apply add_SNo_Lt3 (fL (ordsucc i)) (gL (ordsucc i)) (fL (ordsucc n)) (gL (ordsucc n)) (LfLb i Li) (LgLb i Li) (LfLb n Hn) (LgLb n Hn) to the current goal.
We will prove fL (ordsucc i) < fL (ordsucc n).
An exact proof term for the current goal is HfL3 (ordsucc n) (omega_ordsucc n Hn) (ordsucc i) (nat_ordsucc_in_ordsucc n (omega_nat_p n Hn) i Hi).
We will prove gL (ordsucc i) < gL (ordsucc n).
An exact proof term for the current goal is HgL3 (ordsucc n) (omega_ordsucc n Hn) (ordsucc i) (nat_ordsucc_in_ordsucc n (omega_nat_p n Hn) i Hi).
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 will prove (fR (ordsucc n) + gR (ordsucc n)) + - eps_ n < x + y.
rewrite the current goal using eps_ordsucc_half_add n (omega_nat_p n Hn) (from right to left).
We will prove (fR (ordsucc n) + gR (ordsucc n)) + - (eps_ (ordsucc n) + eps_ (ordsucc n)) < x + y.
We prove the intermediate claim LeSn: SNo (eps_ (ordsucc n)).
An exact proof term for the current goal is SNo_eps_ (ordsucc n) (omega_ordsucc n Hn).
We prove the intermediate claim LmeSn: SNo (- eps_ (ordsucc n)).
An exact proof term for the current goal is SNo_minus_SNo (eps_ (ordsucc n)) LeSn.
rewrite the current goal using minus_add_SNo_distr (eps_ (ordsucc n)) (eps_ (ordsucc n)) LeSn LeSn (from left to right).
We will prove (fR (ordsucc n) + gR (ordsucc n)) + (- eps_ (ordsucc n) + - eps_ (ordsucc n)) < x + y.
rewrite the current goal using add_SNo_com_4_inner_mid (fR (ordsucc n)) (gR (ordsucc n)) (- eps_ (ordsucc n)) (- eps_ (ordsucc n)) (LfRb n Hn) (LgRb n Hn) LmeSn LmeSn (from left to right).
We will prove (fR (ordsucc n) + - eps_ (ordsucc n)) + (gR (ordsucc n) + - eps_ (ordsucc n)) < x + y.
Apply add_SNo_Lt3 (fR (ordsucc n) + - eps_ (ordsucc n)) (gR (ordsucc n) + - eps_ (ordsucc n)) x y (SNo_add_SNo (fR (ordsucc n)) (- eps_ (ordsucc n)) (LfRb n Hn) LmeSn) (SNo_add_SNo (gR (ordsucc n)) (- eps_ (ordsucc n)) (LgRb n Hn) LmeSn) Lx Ly to the current goal.
We will prove fR (ordsucc n) + - eps_ (ordsucc n) < x.
An exact proof term for the current goal is HfR1 (ordsucc n) (omega_ordsucc n Hn).
We will prove gR (ordsucc n) + - eps_ (ordsucc n) < y.
An exact proof term for the current goal is HgR1 (ordsucc n) (omega_ordsucc n Hn).
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 will prove x + y < fR (ordsucc n) + gR (ordsucc n).
Apply add_SNo_Lt3 x y (fR (ordsucc n)) (gR (ordsucc n)) Lx Ly (LfRb n Hn) (LgRb n Hn) to the current goal.
We will prove x < fR (ordsucc n).
An exact proof term for the current goal is HfR2 (ordsucc n) (omega_ordsucc n Hn).
We will prove y < gR (ordsucc n).
An exact proof term for the current goal is HgR2 (ordsucc n) (omega_ordsucc n Hn).
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 ∈ ω.
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 LhR i Li (from left to right).
We will prove fR (ordsucc n) + gR (ordsucc n) < fR (ordsucc i) + gR (ordsucc i).
Apply add_SNo_Lt3 (fR (ordsucc n)) (gR (ordsucc n)) (fR (ordsucc i)) (gR (ordsucc i)) (LfRb n Hn) (LgRb n Hn) (LfRb i Li) (LgRb i Li) to the current goal.
We will prove fR (ordsucc n) < fR (ordsucc i).
An exact proof term for the current goal is HfR3 (ordsucc n) (omega_ordsucc n Hn) (ordsucc i) (nat_ordsucc_in_ordsucc n (omega_nat_p n Hn) i Hi).
We will prove gR (ordsucc n) < gR (ordsucc i).
An exact proof term for the current goal is HgR3 (ordsucc n) (omega_ordsucc n Hn) (ordsucc i) (nat_ordsucc_in_ordsucc n (omega_nat_p n Hn) i Hi).
We prove the intermediate claim LLR: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw.
Apply ReplE_impred ω (λn ⇒ hL n) w Hw to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hwn: w = hL n.
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.
Apply ReplE_impred ω (λn ⇒ hR n) z Hz to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hzm: z = hR m.
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.
Apply ReplE_impred ω (λn ⇒ hL n) w Hw to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hwn: w = hL n.
rewrite the current goal using Hwn (from left to right).
Apply ReplE_impred ω (λn ⇒ hR n) z Hz to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hzm: z = hR m.
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.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
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).
We will prove SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) = SNoCut L R.
Apply SNoCut_ext ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) L R (add_SNo_SNoCutP x y Lx Ly) LLR to the current goal.
We will prove ∀w ∈ {w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}, w < SNoCut L R.
Let w be given.
Assume Hw.
Apply binunionE {w + y|w ∈ SNoL x} {x + w|w ∈ SNoL y} w Hw to the current goal.
Assume Hw: w ∈ {w + y|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL x.
Assume Hww'.
rewrite the current goal using Hww' (from left to right).
We will prove w' + y < SNoCut L R.
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_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega x Hx w' Hw'1 Hw'2.
We prove the intermediate claim Lw'2: ∃n ∈ ω, w' + y ≤ hL n.
Apply dneg to the current goal.
Assume HC: ¬ (∃n ∈ ω, w' + y ≤ hL n).
We prove the intermediate claim Lw'2a: 0 < x + - w'.
Apply SNoLt_minus_pos w' x Hw'1 Lx Hw'3 to the current goal.
We prove the intermediate claim Lw'2b: w' = x.
Apply Lx2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk.
We will prove abs_SNo (w' + - x) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap w' x Hw'1 Lx (from left to right).
We will prove abs_SNo (x + - w') < eps_ k.
rewrite the current goal using pos_abs_SNo (x + - w') Lw'2a (from left to right).
We will prove x + - w' < eps_ k.
Apply add_SNo_minus_Lt1b x w' (eps_ k) Lx Hw'1 (SNo_eps_ k Hk) to the current goal.
We will prove x < eps_ k + w'.
Apply SNoLtLe_or x (eps_ k + w') Lx (SNo_add_SNo (eps_ k) w' (SNo_eps_ k Hk) Hw'1) to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: eps_ k + w' ≤ x.
We will prove False.
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.
Apply SNoLtLe to the current goal.
We will prove w' + y < hL k.
Apply add_SNo_Lt1_cancel (w' + y) (eps_ k) (hL k) (SNo_add_SNo w' y Hw'1 Ly) (SNo_eps_ k Hk) (LhLb k Hk) to the current goal.
We will prove (w' + y) + eps_ k < hL k + eps_ k.
Apply SNoLeLt_tra ((w' + y) + eps_ k) (x + y) (hL k + eps_ k) (SNo_add_SNo (w' + y) (eps_ k) (SNo_add_SNo w' y Hw'1 Ly) (SNo_eps_ k Hk)) Lxy (SNo_add_SNo (hL k) (eps_ k) (LhLb k Hk) (SNo_eps_ k Hk)) to the current goal.
We will prove (w' + y) + eps_ k ≤ x + y.
rewrite the current goal using add_SNo_com_3b_1_2 w' y (eps_ k) Hw'1 Ly (SNo_eps_ k Hk) (from left to right).
We will prove (w' + eps_ k) + y ≤ x + y.
Apply add_SNo_Le1 (w' + eps_ k) y x (SNo_add_SNo w' (eps_ k) Hw'1 (SNo_eps_ k Hk)) Ly Lx to the current goal.
We will prove w' + eps_ k ≤ x.
rewrite the current goal using add_SNo_com w' (eps_ k) Hw'1 (SNo_eps_ k Hk) (from left to right).
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.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
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.
Apply SNoLeLt_tra (w' + y) (hL n) (SNoCut L R) (SNo_add_SNo w' y Hw'1 Ly) (LhLb n Hn1) HLR1 to the current goal.
We will prove w' + y ≤ hL n.
An exact proof term for the current goal is Hn2.
We will prove hL n < SNoCut L R.
Apply HLR3 to the current goal.
We will prove hL n ∈ L.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
Assume Hw: w ∈ {x + w|w ∈ SNoL y}.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL y.
Assume Hww'.
rewrite the current goal using Hww' (from left to right).
We will prove x + w' < SNoCut L R.
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_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega y Hy w' Hw'1 Hw'2.
We prove the intermediate claim Lw'2: ∃n ∈ ω, x + w' ≤ hL n.
Apply dneg to the current goal.
Assume HC: ¬ (∃n ∈ ω, x + w' ≤ hL n).
We prove the intermediate claim Lw'2a: 0 < y + - w'.
Apply SNoLt_minus_pos w' y Hw'1 Ly Hw'3 to the current goal.
We prove the intermediate claim Lw'2b: w' = y.
Apply Ly2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk.
We will prove abs_SNo (w' + - y) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap w' y Hw'1 Ly (from left to right).
We will prove abs_SNo (y + - w') < eps_ k.
rewrite the current goal using pos_abs_SNo (y + - w') Lw'2a (from left to right).
We will prove y + - w' < eps_ k.
Apply add_SNo_minus_Lt1b y w' (eps_ k) Ly Hw'1 (SNo_eps_ k Hk) to the current goal.
We will prove y < eps_ k + w'.
Apply SNoLtLe_or y (eps_ k + w') Ly (SNo_add_SNo (eps_ k) w' (SNo_eps_ k Hk) Hw'1) to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: eps_ k + w' ≤ y.
We will prove False.
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.
Apply SNoLtLe to the current goal.
We will prove x + w' < hL k.
Apply add_SNo_Lt1_cancel (x + w') (eps_ k) (hL k) (SNo_add_SNo x w' Lx Hw'1) (SNo_eps_ k Hk) (LhLb k Hk) to the current goal.
We will prove (x + w') + eps_ k < hL k + eps_ k.
Apply SNoLeLt_tra ((x + w') + eps_ k) (x + y) (hL k + eps_ k) (SNo_add_SNo (x + w') (eps_ k) (SNo_add_SNo x w' Lx Hw'1) (SNo_eps_ k Hk)) Lxy (SNo_add_SNo (hL k) (eps_ k) (LhLb k Hk) (SNo_eps_ k Hk)) to the current goal.
We will prove (x + w') + eps_ k ≤ x + y.
rewrite the current goal using add_SNo_assoc x w' (eps_ k) Lx Hw'1 (SNo_eps_ k Hk) (from right to left).
We will prove x + (w' + eps_ k) ≤ x + y.
Apply add_SNo_Le2 x (w' + eps_ k) y Lx (SNo_add_SNo w' (eps_ k) Hw'1 (SNo_eps_ k Hk)) Ly to the current goal.
We will prove w' + eps_ k ≤ y.
rewrite the current goal using add_SNo_com w' (eps_ k) Hw'1 (SNo_eps_ k Hk) (from left to right).
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.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
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.
Apply SNoLeLt_tra (x + w') (hL n) (SNoCut L R) (SNo_add_SNo x w' Lx Hw'1) (LhLb n Hn1) HLR1 to the current goal.
We will prove x + w' ≤ hL n.
An exact proof term for the current goal is Hn2.
We will prove hL n < SNoCut L R.
Apply HLR3 to the current goal.
We will prove hL n ∈ L.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1.
We will prove ∀z ∈ {z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}, SNoCut L R < z.
Let z be given.
Assume Hz.
Apply binunionE {z + y|z ∈ SNoR x} {x + z|z ∈ SNoR y} z Hz to the current goal.
Assume Hz: z ∈ {z + y|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR x.
Assume Hzz'.
rewrite the current goal using Hzz' (from left to right).
We will prove SNoCut L R < z' + y.
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_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega x Hx z' Hz'1 Hz'2.
We prove the intermediate claim Lz'2: ∃n ∈ ω, hR n ≤ z' + y.
Apply dneg to the current goal.
Assume HC: ¬ (∃n ∈ ω, hR n ≤ z' + y).
We prove the intermediate claim Lz'2a: 0 < z' + - x.
Apply SNoLt_minus_pos x z' Lx Hz'1 Hz'3 to the current goal.
We prove the intermediate claim Lz'2b: z' = x.
Apply Lx2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk.
We will prove abs_SNo (z' + - x) < eps_ k.
rewrite the current goal using pos_abs_SNo (z' + - x) Lz'2a (from left to right).
We will prove z' + - x < eps_ k.
Apply add_SNo_minus_Lt1b z' x (eps_ k) Hz'1 Lx (SNo_eps_ k Hk) to the current goal.
We will prove z' < eps_ k + x.
Apply SNoLtLe_or z' (eps_ k + x) Hz'1 (SNo_add_SNo (eps_ k) x (SNo_eps_ k Hk) Lx) to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: eps_ k + x ≤ z'.
We will prove False.
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.
Apply SNoLtLe to the current goal.
Apply add_SNo_Lt1_cancel (hR k) (- eps_ k) (z' + y) (LhRb k Hk) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk)) (SNo_add_SNo z' y Hz'1 Ly) to the current goal.
We will prove hR k + - eps_ k < (z' + y) + - eps_ k.
Apply SNoLtLe_tra (hR k + - eps_ k) (x + y) ((z' + y) + - eps_ k) (SNo_add_SNo (hR k) (- eps_ k) (LhRb k Hk) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk))) Lxy (SNo_add_SNo (z' + y) (- eps_ k) (SNo_add_SNo z' y Hz'1 Ly) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk))) to the current goal.
We will prove hR k + - eps_ k < x + y.
An exact proof term for the current goal is L6 k Hk.
We will prove x + y ≤ (z' + y) + - eps_ k.
Apply add_SNo_minus_Le2b (z' + y) (eps_ k) (x + y) (SNo_add_SNo z' y Hz'1 Ly) (SNo_eps_ k Hk) Lxy to the current goal.
We will prove (x + y) + eps_ k ≤ z' + y.
rewrite the current goal using add_SNo_com_3b_1_2 x y (eps_ k) Lx Ly (SNo_eps_ k Hk) (from left to right).
We will prove (x + eps_ k) + y ≤ z' + y.
Apply add_SNo_Le1 (x + eps_ k) y z' (SNo_add_SNo x (eps_ k) Lx (SNo_eps_ k Hk)) Ly Hz'1 to the current goal.
We will prove x + eps_ k ≤ z'.
rewrite the current goal using add_SNo_com x (eps_ k) Lx (SNo_eps_ k Hk) (from left to right).
An exact proof term for the current goal is H2.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
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 SNoLtLe_tra (SNoCut L R) (hR n) (z' + y) HLR1 (LhRb n Hn1) (SNo_add_SNo z' y Hz'1 Ly) to the current goal.
We will prove SNoCut L R < hR n.
Apply HLR4 to the current goal.
We will prove hR n ∈ R.
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.
Assume Hz: z ∈ {x + z|z ∈ SNoR y}.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR y.
Assume Hzz'.
rewrite the current goal using Hzz' (from left to right).
We will prove SNoCut L R < x + z'.
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_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega y Hy z' Hz'1 Hz'2.
We prove the intermediate claim Lz'2: ∃n ∈ ω, hR n ≤ x + z'.
Apply dneg to the current goal.
Assume HC: ¬ (∃n ∈ ω, hR n ≤ x + z').
We prove the intermediate claim Lz'2a: 0 < z' + - y.
Apply SNoLt_minus_pos y z' Ly Hz'1 Hz'3 to the current goal.
We prove the intermediate claim Lz'2b: z' = y.
Apply Ly2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk.
We will prove abs_SNo (z' + - y) < eps_ k.
rewrite the current goal using pos_abs_SNo (z' + - y) Lz'2a (from left to right).
We will prove z' + - y < eps_ k.
Apply add_SNo_minus_Lt1b z' y (eps_ k) Hz'1 Ly (SNo_eps_ k Hk) to the current goal.
We will prove z' < eps_ k + y.
Apply SNoLtLe_or z' (eps_ k + y) Hz'1 (SNo_add_SNo (eps_ k) y (SNo_eps_ k Hk) Ly) to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: eps_ k + y ≤ z'.
We will prove False.
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'.
Apply SNoLtLe to the current goal.
Apply add_SNo_Lt1_cancel (hR k) (- eps_ k) (x + z') (LhRb k Hk) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk)) (SNo_add_SNo x z' Lx Hz'1) to the current goal.
We will prove hR k + - eps_ k < (x + z') + - eps_ k.
Apply SNoLtLe_tra (hR k + - eps_ k) (x + y) ((x + z') + - eps_ k) (SNo_add_SNo (hR k) (- eps_ k) (LhRb k Hk) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk))) Lxy (SNo_add_SNo (x + z') (- eps_ k) (SNo_add_SNo x z' Lx Hz'1) (SNo_minus_SNo (eps_ k) (SNo_eps_ k Hk))) to the current goal.
We will prove hR k + - eps_ k < x + y.
An exact proof term for the current goal is L6 k Hk.
We will prove x + y ≤ (x + z') + - eps_ k.
Apply add_SNo_minus_Le2b (x + z') (eps_ k) (x + y) (SNo_add_SNo x z' Lx Hz'1) (SNo_eps_ k Hk) Lxy to the current goal.
We will prove (x + y) + eps_ k ≤ x + z'.
rewrite the current goal using add_SNo_assoc x y (eps_ k) Lx Ly (SNo_eps_ k Hk) (from right to left).
We will prove x + (y + eps_ k) ≤ x + z'.
Apply add_SNo_Le2 x (y + eps_ k) z' Lx (SNo_add_SNo y (eps_ k) Ly (SNo_eps_ k Hk)) Hz'1 to the current goal.
We will prove y + eps_ k ≤ z'.
rewrite the current goal using add_SNo_com y (eps_ k) Ly (SNo_eps_ k Hk) (from left to right).
An exact proof term for the current goal is H2.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
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 SNoLtLe_tra (SNoCut L R) (hR n) (x + z') HLR1 (LhRb n Hn1) (SNo_add_SNo x z' Lx Hz'1) to the current goal.
We will prove SNoCut L R < hR n.
Apply HLR4 to the current goal.
We will prove hR n ∈ R.
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.
Assume Hw: w ∈ L.
rewrite the current goal using add_SNo_eq x Lx y Ly (from right to left).
We will prove w < x + y.
Apply ReplE_impred ω (λn ⇒ hL n) w Hw to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hwn: w = hL n.
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.
Assume Hz: z ∈ R.
rewrite the current goal using add_SNo_eq x Lx y Ly (from right to left).
We will prove x + y < z.
Apply ReplE_impred ω (λn ⇒ hR n) z Hz to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hzn: z = hR n.
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.
An exact proof term for the current goal is SNo_approx_real (x + y) (SNo_add_SNo x y Lx Ly) hL L1 hR L2 L3 L4 L5 L7 L8 L9.
∎