Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hx0 Hy0.
Apply dneg to the current goal.
Assume HC: x * y ∉ real.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7.
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2 Hy3 Hy4 Hy5 Hy6 Hy7.
We prove the intermediate claim Lx7: ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p.
An exact proof term for the current goal is SNo_prereal_incr_lower_pos x Hx1 Hx0 Hx6 Hx7.
We prove the intermediate claim Ly7: ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < y → y < q + eps_ k → p) → p.
An exact proof term for the current goal is SNo_prereal_incr_lower_pos y Hy1 Hy0 Hy6 Hy7.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx1 Hy1.
We prove the intermediate claim Lmxy: SNo (- x * y).
An exact proof term for the current goal is SNo_minus_SNo (x * y) Lxy.
We prove the intermediate claim Lxy2: SNoLev (x * y) ∉ ω.
Assume H1: SNoLev (x * y) ∈ ω.
Apply HC to the current goal.
Apply SNoS_omega_real (x * y) to the current goal.
We will prove x * y ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal (x * y) (SNoLev (x * y)) H1 to the current goal.
We will prove SNo_ (SNoLev (x * y)) (x * y).
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Lxy.
We prove the intermediate claim Lxy3: ∀q, SNo q → SNoLev q ∈ ω → SNoLev q ∈ SNoLev (x * y).
Let q be given.
Assume Hq1 Hq2.
Apply ordinal_trichotomy_or_impred (SNoLev q) (SNoLev (x * y)) (SNoLev_ordinal q Hq1) (SNoLev_ordinal (x * y) Lxy) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: SNoLev q = SNoLev (x * y).
We will prove False.
Apply Lxy2 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hq2.
Assume H1: SNoLev (x * y) ∈ SNoLev q.
We will prove False.
Apply Lxy2 to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_p_trans (SNoLev q) (omega_nat_p (SNoLev q) Hq2) (SNoLev (x * y)) H1.
We prove the intermediate claim LLx: SNoL x ⊆ SNoS_ ω.
Let v be given.
Assume Hv.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3.
Apply SNoS_I ω omega_ordinal v (SNoLev v) to the current goal.
We will prove SNoLev v ∈ ω.
Apply ordsuccE ω (SNoLev x) Hx2 to the current goal.
Assume H1: SNoLev x ∈ ω.
An exact proof term for the current goal is omega_TransSet (SNoLev x) H1 (SNoLev v) Hv2.
Assume H1: SNoLev x = ω.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2.
We will prove SNo_ (SNoLev v) v.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim LRx: SNoR x ⊆ SNoS_ ω.
Let v be given.
Assume Hv.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3.
Apply SNoS_I ω omega_ordinal v (SNoLev v) to the current goal.
We will prove SNoLev v ∈ ω.
Apply ordsuccE ω (SNoLev x) Hx2 to the current goal.
Assume H1: SNoLev x ∈ ω.
An exact proof term for the current goal is omega_TransSet (SNoLev x) H1 (SNoLev v) Hv2.
Assume H1: SNoLev x = ω.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2.
We will prove SNo_ (SNoLev v) v.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim LLy: SNoL y ⊆ SNoS_ ω.
Let v be given.
Assume Hv.
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3.
Apply SNoS_I ω omega_ordinal v (SNoLev v) to the current goal.
We will prove SNoLev v ∈ ω.
Apply ordsuccE ω (SNoLev y) Hy2 to the current goal.
Assume H1: SNoLev y ∈ ω.
An exact proof term for the current goal is omega_TransSet (SNoLev y) H1 (SNoLev v) Hv2.
Assume H1: SNoLev y = ω.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2.
We will prove SNo_ (SNoLev v) v.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim LRy: SNoR y ⊆ SNoS_ ω.
Let v be given.
Assume Hv.
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3.
Apply SNoS_I ω omega_ordinal v (SNoLev v) to the current goal.
We will prove SNoLev v ∈ ω.
Apply ordsuccE ω (SNoLev y) Hy2 to the current goal.
Assume H1: SNoLev y ∈ ω.
An exact proof term for the current goal is omega_TransSet (SNoLev y) H1 (SNoLev v) Hv2.
Assume H1: SNoLev y = ω.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2.
We will prove SNo_ (SNoLev v) v.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim LLx2: ∀v ∈ SNoL x, ∀p : prop, (∀k, k ∈ ω → eps_ k ≤ x + - v → p) → p.
Let v be given.
Assume Hv.
Let p be given.
Assume Hp.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply xm (∀k ∈ ω, abs_SNo (v + - x) < eps_ k) to the current goal.
Assume H1.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
rewrite the current goal using Hx6 v (LLx v Hv) H1 (from right to left) at position 1.
We will prove v < x.
An exact proof term for the current goal is Hv3.
Assume H1: ¬ (∀k ∈ ω, abs_SNo (v + - x) < eps_ k).
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (v + - x) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap v x Hv1 Hx1 (from left to right).
We will prove abs_SNo (x + - v) < eps_ k.
rewrite the current goal using pos_abs_SNo (x + - v) (SNoLt_minus_pos v x Hv1 Hx1 Hv3) (from left to right).
We will prove x + - v < eps_ k.
Apply SNoLtLe_or (x + - v) (eps_ k) (SNo_add_SNo x (- v) Hx1 (SNo_minus_SNo v Hv1)) (SNo_eps_ k Hk) to the current goal.
Assume H3: x + - v < eps_ k.
An exact proof term for the current goal is H3.
Assume H3: eps_ k ≤ x + - v.
We will prove False.
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3.
We prove the intermediate claim LRx2: ∀v ∈ SNoR x, ∀p : prop, (∀k, k ∈ ω → eps_ k ≤ v + - x → p) → p.
Let v be given.
Assume Hv.
Let p be given.
Assume Hp.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply xm (∀k ∈ ω, abs_SNo (v + - x) < eps_ k) to the current goal.
Assume H1.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
rewrite the current goal using Hx6 v (LRx v Hv) H1 (from right to left) at position 2.
We will prove x < v.
An exact proof term for the current goal is Hv3.
Assume H1: ¬ (∀k ∈ ω, abs_SNo (v + - x) < eps_ k).
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (v + - x) < eps_ k.
rewrite the current goal using pos_abs_SNo (v + - x) (SNoLt_minus_pos x v Hx1 Hv1 Hv3) (from left to right).
We will prove v + - x < eps_ k.
Apply SNoLtLe_or (v + - x) (eps_ k) (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx1)) (SNo_eps_ k Hk) to the current goal.
Assume H3: v + - x < eps_ k.
An exact proof term for the current goal is H3.
Assume H3: eps_ k ≤ v + - x.
We will prove False.
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3.
We prove the intermediate claim LLy2: ∀v ∈ SNoL y, ∀p : prop, (∀k, k ∈ ω → eps_ k ≤ y + - v → p) → p.
Let v be given.
Assume Hv.
Let p be given.
Assume Hp.
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
Apply xm (∀k ∈ ω, abs_SNo (v + - y) < eps_ k) to the current goal.
Assume H1.
We will prove False.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using Hy6 v (LLy v Hv) H1 (from right to left) at position 1.
We will prove v < y.
An exact proof term for the current goal is Hv3.
Assume H1: ¬ (∀k ∈ ω, abs_SNo (v + - y) < eps_ k).
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (v + - y) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap v y Hv1 Hy1 (from left to right).
We will prove abs_SNo (y + - v) < eps_ k.
rewrite the current goal using pos_abs_SNo (y + - v) (SNoLt_minus_pos v y Hv1 Hy1 Hv3) (from left to right).
We will prove y + - v < eps_ k.
Apply SNoLtLe_or (y + - v) (eps_ k) (SNo_add_SNo y (- v) Hy1 (SNo_minus_SNo v Hv1)) (SNo_eps_ k Hk) to the current goal.
Assume H3: y + - v < eps_ k.
An exact proof term for the current goal is H3.
Assume H3: eps_ k ≤ y + - v.
We will prove False.
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3.
We prove the intermediate claim LRy2: ∀v ∈ SNoR y, ∀p : prop, (∀k, k ∈ ω → eps_ k ≤ v + - y → p) → p.
Let v be given.
Assume Hv.
Let p be given.
Assume Hp.
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: y < v.
Apply xm (∀k ∈ ω, abs_SNo (v + - y) < eps_ k) to the current goal.
Assume H1.
We will prove False.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using Hy6 v (LRy v Hv) H1 (from right to left) at position 2.
We will prove y < v.
An exact proof term for the current goal is Hv3.
Assume H1: ¬ (∀k ∈ ω, abs_SNo (v + - y) < eps_ k).
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (v + - y) < eps_ k.
rewrite the current goal using pos_abs_SNo (v + - y) (SNoLt_minus_pos y v Hy1 Hv1 Hv3) (from left to right).
We will prove v + - y < eps_ k.
Apply SNoLtLe_or (v + - y) (eps_ k) (SNo_add_SNo v (- y) Hv1 (SNo_minus_SNo y Hy1)) (SNo_eps_ k Hk) to the current goal.
Assume H3: v + - y < eps_ k.
An exact proof term for the current goal is H3.
Assume H3: eps_ k ≤ v + - y.
We will prove False.
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3.
Apply mul_SNo_eq_3 x y Hx1 Hy1 to the current goal.
Let L and R be given.
Assume HLR: SNoCutP L R.
Assume HLE: ∀u, u ∈ L → ∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q.
Assume HLI1: ∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L.
Assume HLI2: ∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L.
Assume HRE: ∀u, u ∈ R → ∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q.
Assume HRI1: ∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R.
Assume HRI2: ∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R.
Assume HxyLR: x * y = SNoCut L R.
We prove the intermediate claim L1: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - (x * y)) < eps_ k) → q = x * y.
Let q be given.
Assume Hq1 Hq2.
We will prove q = x * y.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply SNoLt_trichotomy_or_impred q (x * y) Hq1c Lxy to the current goal.
Assume H1: q < x * y.
We will prove False.
We prove the intermediate claim Lq1: q ∈ SNoL (x * y).
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Lxy.
An exact proof term for the current goal is Hq1c.
We will prove SNoLev q ∈ SNoLev (x * y).
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a.
We will prove q < x * y.
An exact proof term for the current goal is H1.
Apply mul_SNo_SNoL_interpolate_impred x y Hx1 Hy1 q Lq1 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _.
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _.
Assume H2: q + v * w ≤ v * y + x * w.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w ?? Hw1.
We prove the intermediate claim Lmxw: SNo (- x * w).
An exact proof term for the current goal is SNo_minus_SNo (x * w) Lxw.
We prove the intermediate claim Lvy: SNo (v * y).
An exact proof term for the current goal is SNo_mul_SNo v y Hv1 ??.
We prove the intermediate claim Lmvy: SNo (- v * y).
An exact proof term for the current goal is SNo_minus_SNo (v * y) Lvy.
We prove the intermediate claim Lxmv: SNo (x + - v).
An exact proof term for the current goal is SNo_add_SNo x (- v) ?? (SNo_minus_SNo v ??).
We prove the intermediate claim Lymw: SNo (y + - w).
An exact proof term for the current goal is SNo_add_SNo y (- w) ?? (SNo_minus_SNo w ??).
Apply LLx2 v Hv to the current goal.
Let k be given.
Assume Hk1: k ∈ ω.
Assume Hk2: eps_ k ≤ x + - v.
Apply LLy2 w Hw to the current goal.
Let k' be given.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: eps_ k' ≤ y + - w.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk1.
We prove the intermediate claim Lek': SNo (eps_ k').
An exact proof term for the current goal is SNo_eps_ k' Hk'1.
We prove the intermediate claim Lkk': k + k' ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk1 k' Hk'1.
We prove the intermediate claim Lekk': SNo (eps_ (k + k')).
An exact proof term for the current goal is SNo_eps_ (k + k') Lkk'.
We prove the intermediate claim Lekek': SNo (eps_ k * eps_ k').
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) (eps_ k') Lek Lek'.
We prove the intermediate claim L1a: abs_SNo (q + - (x * y)) < eps_ (k + k').
An exact proof term for the current goal is Hq2 (k + k') (add_SNo_In_omega k Hk1 k' Hk'1).
We prove the intermediate claim L1b: eps_ (k + k') ≤ abs_SNo (q + - (x * y)).
rewrite the current goal using abs_SNo_dist_swap q (x * y) Hq1c Lxy (from left to right).
We will prove eps_ (k + k') ≤ abs_SNo (x * y + - q).
rewrite the current goal using pos_abs_SNo (x * y + - q) (SNoLt_minus_pos q (x * y) Hq1c Lxy H1) (from left to right).
We will prove eps_ (k + k') ≤ x * y + - q.
Apply add_SNo_minus_Le2b (x * y) q (eps_ (k + k')) Lxy Hq1c Lekk' to the current goal.
We will prove eps_ (k + k') + q ≤ x * y.
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk1 k' Hk'1 (from right to left).
We will prove eps_ k * eps_ k' + q ≤ x * y.
Apply SNoLe_tra (eps_ k * eps_ k' + q) ((x + - v) * (y + - w) + q) (x * y) (SNo_add_SNo (eps_ k * eps_ k') q ?? ??) (SNo_add_SNo ((x + - v) * (y + - w)) q (SNo_mul_SNo (x + - v) (y + - w) Lxmv Lymw) Hq1c) Lxy to the current goal.
We will prove eps_ k * eps_ k' + q ≤ (x + - v) * (y + - w) + q.
Apply add_SNo_Le1 (eps_ k * eps_ k') q ((x + - v) * (y + - w)) Lekek' Hq1c (SNo_mul_SNo (x + - v) (y + - w) Lxmv Lymw) to the current goal.
We will prove eps_ k * eps_ k' ≤ (x + - v) * (y + - w).
Apply nonneg_mul_SNo_Le2 (eps_ k) (eps_ k') (x + - v) (y + - w) Lek Lek' Lxmv Lymw to the current goal.
We will prove 0 ≤ eps_ k.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k Hk1.
We will prove 0 ≤ eps_ k'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k' Hk'1.
We will prove eps_ k ≤ x + - v.
An exact proof term for the current goal is Hk2.
We will prove eps_ k' ≤ y + - w.
An exact proof term for the current goal is Hk'2.
We will prove (x + - v) * (y + - w) + q ≤ x * y.
rewrite the current goal using SNo_foil_mm x v y w Hx1 Hv1 Hy1 Hw1 (from left to right).
We will prove (x * y + - x * w + - v * y + v * w) + q ≤ x * y.
rewrite the current goal using add_SNo_assoc_4 (x * y) (- x * w) (- v * y) (v * w) ?? ?? ?? ?? (from left to right).
We will prove ((x * y + - x * w + - v * y) + v * w) + q ≤ x * y.
rewrite the current goal using add_SNo_assoc (x * y + - x * w + - v * y) (v * w) q (SNo_add_SNo_3 (x * y) (- x * w) (- v * y) ?? ?? ??) ?? Hq1c (from right to left).
We will prove (x * y + - x * w + - v * y) + (v * w + q) ≤ x * y.
rewrite the current goal using add_SNo_com (v * w) q ?? Hq1c (from left to right).
We will prove (x * y + - x * w + - v * y) + (q + v * w) ≤ x * y.
Apply SNoLe_tra ((x * y + - x * w + - v * y) + (q + v * w)) ((x * y + - x * w + - v * y) + (v * y + x * w)) (x * y) (SNo_add_SNo (x * y + - x * w + - v * y) (q + v * w) (SNo_add_SNo_3 (x * y) (- x * w) (- v * y) ?? ?? ??) (SNo_add_SNo q (v * w) Hq1c ??)) (SNo_add_SNo (x * y + - x * w + - v * y) (v * y + x * w) (SNo_add_SNo_3 (x * y) (- x * w) (- v * y) ?? ?? ??) (SNo_add_SNo (v * y) (x * w) ?? ??)) (SNo_mul_SNo x y Hx1 Hy1) to the current goal.
We will prove (x * y + - x * w + - v * y) + (q + v * w) ≤ (x * y + - x * w + - v * y) + (v * y + x * w).
An exact proof term for the current goal is add_SNo_Le2 (x * y + - x * w + - v * y) (q + v * w) (v * y + x * w) (SNo_add_SNo_3 (x * y) (- x * w) (- v * y) ?? ?? ??) (SNo_add_SNo q (v * w) Hq1c ??) (SNo_add_SNo (v * y) (x * w) ?? ??) H2.
We will prove (x * y + - x * w + - v * y) + (v * y + x * w) ≤ x * y.
rewrite the current goal using add_SNo_minus_SNo_prop5 (x * y) (- x * w) (v * y) (x * w) ?? ?? ?? ?? (from left to right).
We will prove x * y + - x * w + x * w ≤ x * y.
rewrite the current goal using add_SNo_minus_SNo_linv (x * w) ?? (from left to right).
We will prove x * y + 0 ≤ x * y.
rewrite the current goal using add_SNo_0R (x * y) ?? (from left to right).
We will prove x * y ≤ x * y.
Apply SNoLe_ref to the current goal.
Apply SNoLt_irref (eps_ (k + k')) to the current goal.
We will prove eps_ (k + k') < eps_ (k + k').
An exact proof term for the current goal is SNoLeLt_tra (eps_ (k + k')) (abs_SNo (q + - (x * y))) (eps_ (k + k')) Lekk' (SNo_abs_SNo (q + - (x * y)) (SNo_add_SNo q (- (x * y)) Hq1c ??)) Lekk' L1b L1a.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _.
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _.
Assume H2: q + v * w ≤ v * y + x * w.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w ?? Hw1.
We prove the intermediate claim Lmxw: SNo (- x * w).
An exact proof term for the current goal is SNo_minus_SNo (x * w) Lxw.
We prove the intermediate claim Lvy: SNo (v * y).
An exact proof term for the current goal is SNo_mul_SNo v y Hv1 ??.
We prove the intermediate claim Lmvy: SNo (- v * y).
An exact proof term for the current goal is SNo_minus_SNo (v * y) Lvy.
We prove the intermediate claim Lvmx: SNo (v + - x).
An exact proof term for the current goal is SNo_add_SNo v (- x) ?? (SNo_minus_SNo x ??).
We prove the intermediate claim Lwmy: SNo (w + - y).
An exact proof term for the current goal is SNo_add_SNo w (- y) ?? (SNo_minus_SNo y ??).
Apply LRx2 v Hv to the current goal.
Let k be given.
Assume Hk1: k ∈ ω.
Assume Hk2: eps_ k ≤ v + - x.
Apply LRy2 w Hw to the current goal.
Let k' be given.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: eps_ k' ≤ w + - y.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk1.
We prove the intermediate claim Lek': SNo (eps_ k').
An exact proof term for the current goal is SNo_eps_ k' Hk'1.
We prove the intermediate claim Lkk': k + k' ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk1 k' Hk'1.
We prove the intermediate claim Lekk': SNo (eps_ (k + k')).
An exact proof term for the current goal is SNo_eps_ (k + k') Lkk'.
We prove the intermediate claim Lekek': SNo (eps_ k * eps_ k').
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) (eps_ k') Lek Lek'.
We prove the intermediate claim L1c: abs_SNo (q + - (x * y)) < eps_ (k + k').
An exact proof term for the current goal is Hq2 (k + k') (add_SNo_In_omega k Hk1 k' Hk'1).
We prove the intermediate claim L1d: eps_ (k + k') ≤ abs_SNo (q + - (x * y)).
rewrite the current goal using abs_SNo_dist_swap q (x * y) Hq1c Lxy (from left to right).
We will prove eps_ (k + k') ≤ abs_SNo (x * y + - q).
rewrite the current goal using pos_abs_SNo (x * y + - q) (SNoLt_minus_pos q (x * y) Hq1c Lxy H1) (from left to right).
We will prove eps_ (k + k') ≤ x * y + - q.
Apply add_SNo_minus_Le2b (x * y) q (eps_ (k + k')) Lxy Hq1c Lekk' to the current goal.
We will prove eps_ (k + k') + q ≤ x * y.
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk1 k' Hk'1 (from right to left).
We will prove eps_ k * eps_ k' + q ≤ x * y.
Apply SNoLe_tra (eps_ k * eps_ k' + q) ((v + - x) * (w + - y) + q) (x * y) (SNo_add_SNo (eps_ k * eps_ k') q ?? Hq1c) (SNo_add_SNo ((v + - x) * (w + - y)) q (SNo_mul_SNo (v + - x) (w + - y) ?? ??) Hq1c) Lxy to the current goal.
We will prove eps_ k * eps_ k' + q ≤ (v + - x) * (w + - y) + q.
Apply add_SNo_Le1 (eps_ k * eps_ k') q ((v + - x) * (w + - y)) Lekek' Hq1c (SNo_mul_SNo (v + - x) (w + - y) ?? ??) to the current goal.
We will prove eps_ k * eps_ k' ≤ (v + - x) * (w + - y).
Apply nonneg_mul_SNo_Le2 (eps_ k) (eps_ k') (v + - x) (w + - y) Lek Lek' ?? ?? to the current goal.
We will prove 0 ≤ eps_ k.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k Hk1.
We will prove 0 ≤ eps_ k'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k' Hk'1.
We will prove eps_ k ≤ v + - x.
An exact proof term for the current goal is Hk2.
We will prove eps_ k' ≤ w + - y.
An exact proof term for the current goal is Hk'2.
We will prove (v + - x) * (w + - y) + q ≤ x * y.
rewrite the current goal using SNo_foil_mm v x w y Hv1 Hx1 Hw1 Hy1 (from left to right).
We will prove (v * w + - v * y + - x * w + x * y) + q ≤ x * y.
rewrite the current goal using add_SNo_assoc_4 (v * w) (- v * y) (- x * w) (x * y) ?? ?? ?? ?? (from left to right).
We will prove ((v * w + - v * y + - x * w) + x * y) + q ≤ x * y.
rewrite the current goal using add_SNo_assoc (v * w + - v * y + - x * w) (x * y) q (SNo_add_SNo_3 (v * w) (- v * y) (- x * w) ?? ?? ??) ?? Hq1c (from right to left).
We will prove (v * w + - v * y + - x * w) + (x * y + q) ≤ x * y.
rewrite the current goal using add_SNo_com (x * y) q ?? Hq1c (from left to right).
We will prove (v * w + - v * y + - x * w) + (q + x * y) ≤ x * y.
rewrite the current goal using add_SNo_3a_2b (v * w) (- v * y) (- x * w) q (x * y) ?? ?? ?? ?? ?? (from left to right).
We will prove (x * y + - v * y + - x * w) + (q + v * w) ≤ x * y.
Apply SNoLe_tra ((x * y + - v * y + - x * w) + (q + v * w)) ((x * y + - v * y + - x * w) + (v * y + x * w)) (x * y) (SNo_add_SNo (x * y + - v * y + - x * w) (q + v * w) (SNo_add_SNo_3 (x * y) (- v * y) (- x * w) ?? ?? ??) (SNo_add_SNo q (v * w) ?? ??)) (SNo_add_SNo (x * y + - v * y + - x * w) (v * y + x * w) (SNo_add_SNo_3 (x * y) (- v * y) (- x * w) ?? ?? ??) (SNo_add_SNo (v * y) (x * w) ?? ??)) ?? to the current goal.
We will prove (x * y + - v * y + - x * w) + (q + v * w) ≤ (x * y + - v * y + - x * w) + (v * y + x * w).
Apply add_SNo_Le2 (x * y + - v * y + - x * w) (q + v * w) (v * y + x * w) (SNo_add_SNo_3 (x * y) (- v * y) (- x * w) ?? ?? ??) (SNo_add_SNo q (v * w) ?? ??) (SNo_add_SNo (v * y) (x * w) ?? ??) to the current goal.
We will prove q + v * w ≤ v * y + x * w.
An exact proof term for the current goal is H2.
We will prove (x * y + - v * y + - x * w) + (v * y + x * w) ≤ x * y.
rewrite the current goal using add_SNo_com (v * y) (x * w) ?? ?? (from left to right).
We will prove (x * y + - v * y + - x * w) + (x * w + v * y) ≤ x * y.
rewrite the current goal using add_SNo_minus_SNo_prop5 (x * y) (- v * y) (x * w) (v * y) ?? ?? ?? ?? (from left to right).
We will prove x * y + - v * y + v * y ≤ x * y.
rewrite the current goal using add_SNo_minus_SNo_linv (v * y) ?? (from left to right).
We will prove x * y + 0 ≤ x * y.
rewrite the current goal using add_SNo_0R (x * y) ?? (from left to right).
Apply SNoLe_ref to the current goal.
Apply SNoLt_irref (eps_ (k + k')) to the current goal.
We will prove eps_ (k + k') < eps_ (k + k').
An exact proof term for the current goal is SNoLeLt_tra (eps_ (k + k')) (abs_SNo (q + - (x * y))) (eps_ (k + k')) Lekk' (SNo_abs_SNo (q + - (x * y)) (SNo_add_SNo q (- (x * y)) Hq1c (SNo_minus_SNo (x * y) Lxy))) Lekk' L1d L1c.
Assume H1: q = x * y.
An exact proof term for the current goal is H1.
Assume H1: x * y < q.
We will prove False.
We prove the intermediate claim Lq2: q ∈ SNoR (x * y).
Apply SNoR_I to the current goal.
An exact proof term for the current goal is Lxy.
An exact proof term for the current goal is Hq1c.
We will prove SNoLev q ∈ SNoLev (x * y).
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a.
We will prove x * y < q.
An exact proof term for the current goal is H1.
Apply mul_SNo_SNoR_interpolate_impred x y Hx1 Hy1 q Lq2 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _.
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _.
Assume H2: v * y + x * w ≤ q + v * w.
We prove the intermediate claim Lvy: SNo (v * y).
An exact proof term for the current goal is SNo_mul_SNo v y Hv1 Hy1.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w ?? Hw1.
We prove the intermediate claim Lmxw: SNo (- x * w).
An exact proof term for the current goal is SNo_minus_SNo (x * w) Lxw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 ??.
We prove the intermediate claim Lmvw: SNo (- v * w).
An exact proof term for the current goal is SNo_minus_SNo (v * w) Lvw.
We prove the intermediate claim Lxmv: SNo (x + - v).
An exact proof term for the current goal is SNo_add_SNo x (- v) ?? (SNo_minus_SNo v ??).
We prove the intermediate claim Lwmy: SNo (w + - y).
An exact proof term for the current goal is SNo_add_SNo w (- y) ?? (SNo_minus_SNo y ??).
Apply LLx2 v Hv to the current goal.
Let k be given.
Assume Hk1: k ∈ ω.
Assume Hk2: eps_ k ≤ x + - v.
Apply LRy2 w Hw to the current goal.
Let k' be given.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: eps_ k' ≤ w + - y.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk1.
We prove the intermediate claim Lek': SNo (eps_ k').
An exact proof term for the current goal is SNo_eps_ k' Hk'1.
We prove the intermediate claim Lkk': k + k' ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk1 k' Hk'1.
We prove the intermediate claim Lekk': SNo (eps_ (k + k')).
An exact proof term for the current goal is SNo_eps_ (k + k') Lkk'.
We prove the intermediate claim Lekek': SNo (eps_ k * eps_ k').
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) (eps_ k') Lek Lek'.
We prove the intermediate claim L1e: abs_SNo (q + - (x * y)) < eps_ (k + k').
An exact proof term for the current goal is Hq2 (k + k') (add_SNo_In_omega k Hk1 k' Hk'1).
We prove the intermediate claim L1f: eps_ (k + k') ≤ abs_SNo (q + - (x * y)).
rewrite the current goal using pos_abs_SNo (q + - x * y) (SNoLt_minus_pos (x * y) q Lxy Hq1c H1) (from left to right).
We will prove eps_ (k + k') ≤ q + - x * y.
Apply add_SNo_minus_Le2b q (x * y) (eps_ (k + k')) Hq1c Lxy Lekk' to the current goal.
We will prove eps_ (k + k') + x * y ≤ q.
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk1 k' Hk'1 (from right to left).
We will prove eps_ k * eps_ k' + x * y ≤ q.
Apply SNoLe_tra (eps_ k * eps_ k' + x * y) ((x + - v) * (w + - y) + x * y) q (SNo_add_SNo (eps_ k * eps_ k') (x * y) ?? ??) (SNo_add_SNo ((x + - v) * (w + - y)) (x * y) (SNo_mul_SNo (x + - v) (w + - y) Lxmv Lwmy) Lxy) Hq1c to the current goal.
We will prove eps_ k * eps_ k' + x * y ≤ (x + - v) * (w + - y) + x * y.
Apply add_SNo_Le1 (eps_ k * eps_ k') (x * y) ((x + - v) * (w + - y)) Lekek' Lxy (SNo_mul_SNo (x + - v) (w + - y) Lxmv Lwmy) to the current goal.
We will prove eps_ k * eps_ k' ≤ (x + - v) * (w + - y).
Apply nonneg_mul_SNo_Le2 (eps_ k) (eps_ k') (x + - v) (w + - y) Lek Lek' Lxmv Lwmy to the current goal.
We will prove 0 ≤ eps_ k.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k Hk1.
We will prove 0 ≤ eps_ k'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k' Hk'1.
We will prove eps_ k ≤ x + - v.
An exact proof term for the current goal is Hk2.
We will prove eps_ k' ≤ w + - y.
An exact proof term for the current goal is Hk'2.
We will prove (x + - v) * (w + - y) + x * y ≤ q.
rewrite the current goal using SNo_foil_mm x v w y Hx1 Hv1 Hw1 Hy1 (from left to right).
We will prove (x * w + - x * y + - v * w + v * y) + x * y ≤ q.
rewrite the current goal using add_SNo_rotate_4_1 (- x * y) (- v * w) (v * y) (x * w) ?? ?? ?? ?? (from right to left).
We will prove (- x * y + - v * w + v * y + x * w) + x * y ≤ q.
rewrite the current goal using add_SNo_com (- x * y + - v * w + v * y + x * w) (x * y) (SNo_add_SNo_4 (- x * y) (- v * w) (v * y) (x * w) ?? ?? ?? ??) ?? (from left to right).
rewrite the current goal using add_SNo_minus_L2' (x * y) (- v * w + v * y + x * w) ?? (SNo_add_SNo_3 (- v * w) (v * y) (x * w) ?? ?? ??) (from left to right).
We will prove - v * w + v * y + x * w ≤ q.
Apply SNoLe_tra (- v * w + v * y + x * w) (- v * w + q + v * w) q (SNo_add_SNo_3 (- v * w) (v * y) (x * w) ?? ?? ??) (SNo_add_SNo_3 (- v * w) q (v * w) ?? ?? ??) Hq1c to the current goal.
We will prove - v * w + v * y + x * w ≤ - v * w + q + v * w.
An exact proof term for the current goal is add_SNo_Le2 (- v * w) (v * y + x * w) (q + v * w) ?? (SNo_add_SNo (v * y) (x * w) ?? ??) (SNo_add_SNo q (v * w) Hq1c ??) H2.
We will prove - v * w + q + v * w ≤ q.
rewrite the current goal using add_SNo_com q (v * w) ?? ?? (from left to right).
rewrite the current goal using add_SNo_minus_L2 (v * w) q ?? ?? (from left to right).
We will prove q ≤ q.
Apply SNoLe_ref to the current goal.
Apply SNoLt_irref (eps_ (k + k')) to the current goal.
We will prove eps_ (k + k') < eps_ (k + k').
An exact proof term for the current goal is SNoLeLt_tra (eps_ (k + k')) (abs_SNo (q + - (x * y))) (eps_ (k + k')) Lekk' (SNo_abs_SNo (q + - (x * y)) (SNo_add_SNo q (- (x * y)) Hq1c ??)) Lekk' L1f L1e.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _.
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _.
Assume H2: v * y + x * w ≤ q + v * w.
We prove the intermediate claim Lvy: SNo (v * y).
An exact proof term for the current goal is SNo_mul_SNo v y Hv1 Hy1.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w ?? Hw1.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 ??.
We prove the intermediate claim Lmvw: SNo (- v * w).
An exact proof term for the current goal is SNo_minus_SNo (v * w) Lvw.
We prove the intermediate claim Lvmx: SNo (v + - x).
An exact proof term for the current goal is SNo_add_SNo v (- x) ?? (SNo_minus_SNo x ??).
We prove the intermediate claim Lymw: SNo (y + - w).
An exact proof term for the current goal is SNo_add_SNo y (- w) ?? (SNo_minus_SNo w ??).
Apply LRx2 v Hv to the current goal.
Let k be given.
Assume Hk1: k ∈ ω.
Assume Hk2: eps_ k ≤ v + - x.
Apply LLy2 w Hw to the current goal.
Let k' be given.
Assume Hk'1: k' ∈ ω.
Assume Hk'2: eps_ k' ≤ y + - w.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk1.
We prove the intermediate claim Lek': SNo (eps_ k').
An exact proof term for the current goal is SNo_eps_ k' Hk'1.
We prove the intermediate claim Lkk': k + k' ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk1 k' Hk'1.
We prove the intermediate claim Lekk': SNo (eps_ (k + k')).
An exact proof term for the current goal is SNo_eps_ (k + k') Lkk'.
We prove the intermediate claim Lekek': SNo (eps_ k * eps_ k').
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) (eps_ k') Lek Lek'.
We prove the intermediate claim L1g: abs_SNo (q + - (x * y)) < eps_ (k + k').
An exact proof term for the current goal is Hq2 (k + k') (add_SNo_In_omega k Hk1 k' Hk'1).
We prove the intermediate claim L1h: eps_ (k + k') ≤ abs_SNo (q + - (x * y)).
rewrite the current goal using pos_abs_SNo (q + - x * y) (SNoLt_minus_pos (x * y) q Lxy Hq1c H1) (from left to right).
We will prove eps_ (k + k') ≤ q + - x * y.
Apply add_SNo_minus_Le2b q (x * y) (eps_ (k + k')) Hq1c Lxy Lekk' to the current goal.
We will prove eps_ (k + k') + x * y ≤ q.
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk1 k' Hk'1 (from right to left).
We will prove eps_ k * eps_ k' + x * y ≤ q.
Apply SNoLe_tra (eps_ k * eps_ k' + x * y) ((v + - x) * (y + - w) + x * y) q (SNo_add_SNo (eps_ k * eps_ k') (x * y) ?? Lxy) (SNo_add_SNo ((v + - x) * (y + - w)) (x * y) (SNo_mul_SNo (v + - x) (y + - w) ?? ??) Lxy) Hq1c to the current goal.
We will prove eps_ k * eps_ k' + x * y ≤ (v + - x) * (y + - w) + x * y.
Apply add_SNo_Le1 (eps_ k * eps_ k') (x * y) ((v + - x) * (y + - w)) Lekek' Lxy (SNo_mul_SNo (v + - x) (y + - w) ?? ??) to the current goal.
We will prove eps_ k * eps_ k' ≤ (v + - x) * (y + - w).
Apply nonneg_mul_SNo_Le2 (eps_ k) (eps_ k') (v + - x) (y + - w) Lek Lek' ?? ?? to the current goal.
We will prove 0 ≤ eps_ k.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k Hk1.
We will prove 0 ≤ eps_ k'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k' Hk'1.
We will prove eps_ k ≤ v + - x.
An exact proof term for the current goal is Hk2.
We will prove eps_ k' ≤ y + - w.
An exact proof term for the current goal is Hk'2.
We will prove (v + - x) * (y + - w) + x * y ≤ q.
rewrite the current goal using SNo_foil_mm v x y w Hv1 Hx1 Hy1 Hw1 (from left to right).
We will prove (v * y + - v * w + - x * y + x * w) + x * y ≤ q.
rewrite the current goal using add_SNo_rotate_4_1 (v * y) (- v * w) (- x * y) (x * w) ?? ?? ?? ?? (from left to right).
rewrite the current goal using add_SNo_rotate_4_1 (x * w) (v * y) (- v * w) (- x * y) ?? ?? ?? ?? (from left to right).
We will prove (- x * y + x * w + v * y + - v * w) + x * y ≤ q.
rewrite the current goal using add_SNo_com (- x * y + x * w + v * y + - v * w) (x * y) (SNo_add_SNo_4 (- x * y) (x * w) (v * y) (- v * w) ?? ?? ?? ??) ?? (from left to right).
We will prove x * y + - x * y + x * w + v * y + - v * w ≤ q.
rewrite the current goal using add_SNo_minus_L2' (x * y) (x * w + v * y + - v * w) ?? (SNo_add_SNo_3 (x * w) (v * y) (- v * w) ?? ?? ??) (from left to right).
We will prove x * w + v * y + - v * w ≤ q.
rewrite the current goal using add_SNo_rotate_3_1 (x * w) (v * y) (- v * w) ?? ?? ?? (from left to right).
We will prove - v * w + x * w + v * y ≤ q.
Apply SNoLe_tra (- v * w + x * w + v * y) (- v * w + q + v * w) q (SNo_add_SNo_3 (- v * w) (x * w) (v * y) ?? ?? ??) (SNo_add_SNo_3 (- v * w) q (v * w) ?? ?? ??) ?? to the current goal.
We will prove - v * w + x * w + v * y ≤ - v * w + q + v * w.
Apply add_SNo_Le2 (- v * w) (x * w + v * y) (q + v * w) ?? (SNo_add_SNo (x * w) (v * y) ?? ??) (SNo_add_SNo q (v * w) ?? ??) to the current goal.
We will prove x * w + v * y ≤ q + v * w.
rewrite the current goal using add_SNo_com (x * w) (v * y) ?? ?? (from left to right).
An exact proof term for the current goal is H2.
We will prove - v * w + q + v * w ≤ q.
rewrite the current goal using add_SNo_com q (v * w) ?? ?? (from left to right).
We will prove - v * w + v * w + q ≤ q.
rewrite the current goal using add_SNo_minus_L2 (v * w) q ?? ?? (from left to right).
We will prove q ≤ q.
Apply SNoLe_ref to the current goal.
Apply SNoLt_irref (eps_ (k + k')) to the current goal.
We will prove eps_ (k + k') < eps_ (k + k').
An exact proof term for the current goal is SNoLeLt_tra (eps_ (k + k')) (abs_SNo (q + - (x * y))) (eps_ (k + k')) Lekk' (SNo_abs_SNo (q + - (x * y)) (SNo_add_SNo q (- (x * y)) Hq1c (SNo_minus_SNo (x * y) Lxy))) Lekk' L1h L1g.
We prove the intermediate claim LNex: ∃N ∈ ω, eps_ N * x < 1 ∧ eps_ N * y < 1.
Apply SNoS_ordsucc_omega_bdd_eps_pos x Hx3 Hx0 Hx5 to the current goal.
Let N be given.
Assume HN.
Apply HN to the current goal.
Assume HN1: N ∈ ω.
Assume HN2: eps_ N * x < 1.
Apply SNoS_ordsucc_omega_bdd_eps_pos y Hy3 Hy0 Hy5 to the current goal.
Let N' be given.
Assume HN'.
Apply HN' to the current goal.
Assume HN'1: N' ∈ ω.
Assume HN'2: eps_ N' * y < 1.
Apply ordinal_trichotomy_or_impred N N' (nat_p_ordinal N (omega_nat_p N HN1)) (nat_p_ordinal N' (omega_nat_p N' HN'1)) to the current goal.
Assume H1: N ∈ N'.
We use N' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN'1.
Apply andI to the current goal.
We will prove eps_ N' * x < 1.
Apply SNoLt_tra (eps_ N' * x) (eps_ N * x) 1 (SNo_mul_SNo (eps_ N') x (SNo_eps_ N' HN'1) Hx1) (SNo_mul_SNo (eps_ N) x (SNo_eps_ N HN1) Hx1) SNo_1 to the current goal.
We will prove eps_ N' * x < eps_ N * x.
Apply pos_mul_SNo_Lt' (eps_ N') (eps_ N) x (SNo_eps_ N' HN'1) (SNo_eps_ N HN1) Hx1 Hx0 to the current goal.
We will prove eps_ N' < eps_ N.
An exact proof term for the current goal is SNo_eps_decr N' HN'1 N H1.
An exact proof term for the current goal is HN2.
An exact proof term for the current goal is HN'2.
Assume H1: N = 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.
Apply andI to the current goal.
An exact proof term for the current goal is HN2.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is HN'2.
Assume H1: N' ∈ 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.
Apply andI to the current goal.
An exact proof term for the current goal is HN2.
We will prove eps_ N * y < 1.
Apply SNoLt_tra (eps_ N * y) (eps_ N' * y) 1 (SNo_mul_SNo (eps_ N) y (SNo_eps_ N HN1) Hy1) (SNo_mul_SNo (eps_ N') y (SNo_eps_ N' HN'1) Hy1) SNo_1 to the current goal.
We will prove eps_ N * y < eps_ N' * y.
Apply pos_mul_SNo_Lt' (eps_ N) (eps_ N') y (SNo_eps_ N HN1) (SNo_eps_ N' HN'1) Hy1 Hy0 to the current goal.
We will prove eps_ N < eps_ N'.
An exact proof term for the current goal is SNo_eps_decr N HN1 N' H1.
An exact proof term for the current goal is HN'2.
Apply LNex to the current goal.
Let N be given.
Assume HN.
Apply HN to the current goal.
Assume HN1: N ∈ ω.
Assume HN.
Apply HN to the current goal.
Assume HN2: eps_ N * x < 1.
Assume HN3: eps_ N * y < 1.
We prove the intermediate claim L2: ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x * y ∧ x * y < q + eps_ k.
Let k be given.
Assume Hk.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
We prove the intermediate claim Lk1: k + 1 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk 1 (nat_p_omega 1 nat_1).
We prove the intermediate claim Lk2: k + 2 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk 2 (nat_p_omega 2 nat_2).
Set k' to be the term N + k + 2.
We prove the intermediate claim Lk': k' ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega N HN1 (k + 2) Lk2.
We prove the intermediate claim Lek': SNo (eps_ k').
An exact proof term for the current goal is SNo_eps_ k' Lk'.
Apply Lx7 k' Lk' to the current goal.
Let q be given.
Assume Hq1: q ∈ SNoS_ ω.
Assume Hqpos: 0 < q.
Assume Hq2: q < x.
Assume Hq3: x < q + eps_ k'.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply Ly7 k' Lk' to the current goal.
Let q' be given.
Assume Hq'1: q' ∈ SNoS_ ω.
Assume Hq'pos: 0 < q'.
Assume Hq'2: q' < y.
Assume Hq'3: y < q' + eps_ k'.
Apply SNoS_E2 ω omega_ordinal q' Hq'1 to the current goal.
Assume Hq'1a Hq'1b Hq'1c Hq'1d.
We prove the intermediate claim Lqq': SNo (q * q').
An exact proof term for the current goal is SNo_mul_SNo q q' Hq1c Hq'1c.
We use (q * q') to witness the existential quantifier.
Apply andI to the current goal.
We will prove q * q' ∈ SNoS_ ω.
An exact proof term for the current goal is mul_SNo_SNoS_omega q Hq1 q' Hq'1.
Apply andI to the current goal.
We will prove q * q' < x * y.
An exact proof term for the current goal is pos_mul_SNo_Lt2 q q' x y Hq1c Hq'1c Hx1 Hy1 Hqpos Hq'pos Hq2 Hq'2.
We will prove x * y < q * q' + eps_ k.
Apply SNoLt_tra (x * y) ((q + eps_ k') * (q' + eps_ k')) (q * q' + eps_ k) Lxy (SNo_mul_SNo (q + eps_ k') (q' + eps_ k') (SNo_add_SNo q (eps_ k') Hq1c Lek') (SNo_add_SNo q' (eps_ k') Hq'1c Lek')) (SNo_add_SNo (q * q') (eps_ k) (SNo_mul_SNo q q' Hq1c Hq'1c) Lek) to the current goal.
We will prove x * y < (q + eps_ k') * (q' + eps_ k').
An exact proof term for the current goal is pos_mul_SNo_Lt2 x y (q + eps_ k') (q' + eps_ k') Hx1 Hy1 (SNo_add_SNo q (eps_ k') Hq1c Lek') (SNo_add_SNo q' (eps_ k') Hq'1c Lek') Hx0 Hy0 Hq3 Hq'3.
We will prove (q + eps_ k') * (q' + eps_ k') < q * q' + eps_ k.
rewrite the current goal using SNo_foil q (eps_ k') q' (eps_ k') Hq1c Lek' Hq'1c Lek' (from left to right).
We will prove q * q' + q * eps_ k' + eps_ k' * q' + eps_ k' * eps_ k' < q * q' + eps_ k.
Apply add_SNo_Lt2 (q * q') (q * eps_ k' + eps_ k' * q' + eps_ k' * eps_ k') (eps_ k) Lqq' (SNo_add_SNo_3 (q * eps_ k') (eps_ k' * q') (eps_ k' * eps_ k') (SNo_mul_SNo q (eps_ k') Hq1c Lek') (SNo_mul_SNo (eps_ k') q' Lek' Hq'1c) (SNo_mul_SNo (eps_ k') (eps_ k') Lek' Lek')) Lek to the current goal.
We will prove q * eps_ k' + eps_ k' * q' + eps_ k' * eps_ k' < eps_ k.
We will prove q * eps_ (N + k + 2) + eps_ (N + k + 2) * q' + eps_ (N + k + 2) * eps_ (N + k + 2) < eps_ k.
rewrite the current goal using mul_SNo_eps_eps_add_SNo N HN1 (k + 2) Lk2 (from right to left).
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < eps_ k.
rewrite the current goal using eps_ordsucc_half_add k (omega_nat_p k Hk) (from right to left).
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < eps_ (ordsucc k) + eps_ (ordsucc k).
rewrite the current goal using eps_ordsucc_half_add (ordsucc k) (nat_ordsucc k (omega_nat_p k Hk)) (from right to left) at position 1.
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < (eps_ (ordsucc (ordsucc k)) + eps_ (ordsucc (ordsucc k))) + eps_ (ordsucc k).
rewrite the current goal using add_SNo_1_ordsucc k Hk (from right to left).
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < (eps_ (ordsucc (k + 1)) + eps_ (ordsucc (k + 1))) + eps_ (k + 1).
rewrite the current goal using add_SNo_1_ordsucc (k + 1) (add_SNo_In_omega k Hk 1 (nat_p_omega 1 nat_1)) (from right to left).
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < (eps_ (((k + 1) + 1)) + eps_ (((k + 1) + 1))) + eps_ (k + 1).
rewrite the current goal using add_SNo_assoc k 1 1 (omega_SNo k Hk) SNo_1 SNo_1 (from right to left).
rewrite the current goal using add_SNo_1_1_2 (from left to right).
We will prove q * eps_ N * eps_ (k + 2) + (eps_ N * eps_ (k + 2)) * q' + (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < (eps_ (k + 2) + eps_ (k + 2)) + eps_ (k + 1).
We prove the intermediate claim LeN: SNo (eps_ N).
An exact proof term for the current goal is SNo_eps_ N HN1.
We prove the intermediate claim Lek1: SNo (eps_ (k + 1)).
An exact proof term for the current goal is SNo_eps_ (k + 1) Lk1.
We prove the intermediate claim Lek2: SNo (eps_ (k + 2)).
An exact proof term for the current goal is SNo_eps_ (k + 2) Lk2.
We prove the intermediate claim LeNek2: SNo (eps_ N * eps_ (k + 2)).
An exact proof term for the current goal is SNo_mul_SNo (eps_ N) (eps_ (k + 2)) LeN Lek2.
We prove the intermediate claim LeNek2sq: SNo ((eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2))).
An exact proof term for the current goal is SNo_mul_SNo (eps_ N * eps_ (k + 2)) (eps_ N * eps_ (k + 2)) LeNek2 LeNek2.
rewrite the current goal using add_SNo_assoc (eps_ (k + 2)) (eps_ (k + 2)) (eps_ (k + 1)) Lek2 Lek2 Lek1 (from right to left).
Apply add_SNo_Lt4 (q * eps_ N * eps_ (k + 2)) ((eps_ N * eps_ (k + 2)) * q') ((eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2))) (eps_ (k + 2)) (eps_ (k + 2)) (eps_ (k + 1)) (SNo_mul_SNo q (eps_ N * eps_ (k + 2)) Hq1c LeNek2) (SNo_mul_SNo (eps_ N * eps_ (k + 2)) q' LeNek2 Hq'1c) LeNek2sq Lek2 Lek2 Lek1 to the current goal.
We will prove q * eps_ N * eps_ (k + 2) < eps_ (k + 2).
rewrite the current goal using mul_SNo_assoc q (eps_ N) (eps_ (k + 2)) Hq1c LeN Lek2 (from left to right).
We will prove (q * eps_ N) * eps_ (k + 2) < eps_ (k + 2).
Apply mul_SNo_Lt1_pos_Lt (q * eps_ N) (eps_ (k + 2)) (SNo_mul_SNo q (eps_ N) Hq1c LeN) Lek2 to the current goal.
We will prove q * eps_ N < 1.
Apply SNoLt_tra (q * eps_ N) (x * eps_ N) 1 (SNo_mul_SNo q (eps_ N) Hq1c LeN) (SNo_mul_SNo x (eps_ N) Hx1 LeN) SNo_1 to the current goal.
We will prove q * eps_ N < x * eps_ N.
Apply pos_mul_SNo_Lt' q x (eps_ N) Hq1c Hx1 (SNo_eps_ N HN1) to the current goal.
We will prove 0 < eps_ N.
An exact proof term for the current goal is SNo_eps_pos N HN1.
We will prove q < x.
An exact proof term for the current goal is Hq2.
We will prove x * eps_ N < 1.
rewrite the current goal using mul_SNo_com x (eps_ N) Hx1 LeN (from left to right).
An exact proof term for the current goal is HN2.
We will prove 0 < eps_ (k + 2).
An exact proof term for the current goal is SNo_eps_pos (k + 2) Lk2.
We will prove (eps_ N * eps_ (k + 2)) * q' < eps_ (k + 2).
rewrite the current goal using mul_SNo_com (eps_ N * eps_ (k + 2)) q' (SNo_mul_SNo (eps_ N) (eps_ (k + 2)) LeN Lek2) Hq'1c (from left to right).
We will prove q' * (eps_ N * eps_ (k + 2)) < eps_ (k + 2).
rewrite the current goal using mul_SNo_assoc q' (eps_ N) (eps_ (k + 2)) Hq'1c LeN Lek2 (from left to right).
We will prove (q' * eps_ N) * eps_ (k + 2) < eps_ (k + 2).
Apply mul_SNo_Lt1_pos_Lt (q' * eps_ N) (eps_ (k + 2)) (SNo_mul_SNo q' (eps_ N) Hq'1c LeN) Lek2 to the current goal.
We will prove q' * eps_ N < 1.
Apply SNoLt_tra (q' * eps_ N) (y * eps_ N) 1 (SNo_mul_SNo q' (eps_ N) Hq'1c LeN) (SNo_mul_SNo y (eps_ N) Hy1 LeN) SNo_1 to the current goal.
We will prove q' * eps_ N < y * eps_ N.
Apply pos_mul_SNo_Lt' q' y (eps_ N) Hq'1c Hy1 (SNo_eps_ N HN1) to the current goal.
We will prove 0 < eps_ N.
An exact proof term for the current goal is SNo_eps_pos N HN1.
We will prove q' < y.
An exact proof term for the current goal is Hq'2.
We will prove y * eps_ N < 1.
rewrite the current goal using mul_SNo_com y (eps_ N) Hy1 LeN (from left to right).
An exact proof term for the current goal is HN3.
We will prove 0 < eps_ (k + 2).
An exact proof term for the current goal is SNo_eps_pos (k + 2) Lk2.
We will prove (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) < eps_ (k + 1).
Apply SNoLeLt_tra ((eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2))) (eps_ (k + 2)) (eps_ (k + 1)) LeNek2sq Lek2 Lek1 to the current goal.
We will prove (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) ≤ eps_ (k + 2).
Apply SNoLe_tra ((eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2))) (eps_ N * eps_ (k + 2)) (eps_ (k + 2)) LeNek2sq LeNek2 Lek2 to the current goal.
We will prove (eps_ N * eps_ (k + 2)) * (eps_ N * eps_ (k + 2)) ≤ eps_ N * eps_ (k + 2).
Apply mul_SNo_Le1_nonneg_Le (eps_ N * eps_ (k + 2)) (eps_ N * eps_ (k + 2)) LeNek2 LeNek2 to the current goal.
We will prove eps_ N * eps_ (k + 2) ≤ 1.
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from right to left) at position 2.
We will prove eps_ N * eps_ (k + 2) ≤ 1 * 1.
Apply nonneg_mul_SNo_Le2 (eps_ N) (eps_ (k + 2)) 1 1 LeN Lek2 SNo_1 SNo_1 to the current goal.
We will prove 0 ≤ eps_ N.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos N HN1.
We will prove 0 ≤ eps_ (k + 2).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos (k + 2) Lk2.
We will prove eps_ N ≤ 1.
Apply eps_bd_1 to the current goal.
An exact proof term for the current goal is HN1.
We will prove eps_ (k + 2) ≤ 1.
Apply eps_bd_1 to the current goal.
An exact proof term for the current goal is Lk2.
We will prove 0 ≤ eps_ N * eps_ (k + 2).
Apply SNoLtLe to the current goal.
Apply mul_SNo_pos_pos (eps_ N) (eps_ (k + 2)) LeN Lek2 to the current goal.
An exact proof term for the current goal is SNo_eps_pos N HN1.
An exact proof term for the current goal is SNo_eps_pos (k + 2) Lk2.
We will prove eps_ N * eps_ (k + 2) ≤ eps_ (k + 2).
Apply mul_SNo_Le1_nonneg_Le (eps_ N) (eps_ (k + 2)) LeN Lek2 to the current goal.
We will prove eps_ N ≤ 1.
Apply eps_bd_1 to the current goal.
An exact proof term for the current goal is HN1.
We will prove 0 ≤ eps_ (k + 2).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos (k + 2) Lk2.
We will prove eps_ (k + 2) < eps_ (k + 1).
Apply SNo_eps_decr (k + 2) Lk2 (k + 1) to the current goal.
We will prove k + 1 ∈ k + 2.
Apply ordinal_SNoLt_In (k + 1) (k + 2) (nat_p_ordinal (k + 1) (omega_nat_p (k + 1) Lk1)) (nat_p_ordinal (k + 2) (omega_nat_p (k + 2) Lk2)) to the current goal.
We will prove k + 1 < k + 2.
Apply add_SNo_Lt2 k 1 2 (omega_SNo k Hk) SNo_1 SNo_2 to the current goal.
We will prove 1 < 2.
An exact proof term for the current goal is SNoLt_1_2.
Apply SNo_prereal_incr_lower_approx (x * y) Lxy L1 L2 to the current goal.
Let hL be given.
Assume HhL.
Apply HhL to the current goal.
Assume HhL1: hL ∈ SNoS_ ωω.
Assume HhL2: ∀n ∈ ω, hL n < x * y ∧ x * y < hL n + eps_ n ∧ ∀i ∈ n, hL i < hL n.
Apply SNo_prereal_decr_upper_approx (x * y) Lxy L1 L2 to the current goal.
Let hR be given.
Assume HhR.
Apply HhR to the current goal.
Assume HhR1: hR ∈ SNoS_ ωω.
Assume HhR2: ∀n ∈ ω, hR n + - eps_ n < x * y ∧ x * y < hR n ∧ ∀i ∈ n, hR n < hR i.
We prove the intermediate claim LhL: ∀n ∈ ω, SNo (hL n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (hL n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) hL n HhL1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LhR: ∀n ∈ ω, SNo (hR n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (hR n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) hR n HhR1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim L3: ∀n ∈ ω, hL n < x * y.
Let n be given.
Assume Hn.
Apply HhL2 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 L4: ∀n ∈ ω, x * y < hR n.
Let n be given.
Assume Hn.
Apply HhR2 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 L5: ∀n m ∈ ω, hL n < hR m.
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
Apply SNoLt_tra (hL n) (x * y) (hR m) (LhL n Hn) Lxy (LhR 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 L4 m Hm.
Apply SNo_approx_real_lem hL HhL1 hR HhR1 L5 to the current goal.
Assume HhLR1: SNoCutP {hL n|n ∈ ω} {hR n|n ∈ ω}.
Assume HhLR2: SNo (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}).
Assume _ _.
Assume HhLR5: ∀n ∈ ω, hL n < SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
Assume HhLR6: ∀n ∈ ω, SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω} < hR n.
We prove the intermediate claim L6: ∀n ∈ ω, x * y < hL n + eps_ n.
Let n be given.
Assume Hn.
Apply HhL2 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 L7: ∀n ∈ ω, ∀i ∈ n, hL i < hL n.
Let n be given.
Assume Hn.
Apply HhL2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim L8: ∀n ∈ ω, hR n + - eps_ n < x * y.
Let n be given.
Assume Hn.
Apply HhR2 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 L9: ∀n ∈ ω, ∀i ∈ n, hR n < hR i.
Let n be given.
Assume Hn.
Apply HhR2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim L10: x * y = SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
rewrite the current goal using HxyLR (from left to right).
We will prove SNoCut L R = SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
Apply SNoCut_ext L R {hL n|n ∈ ω} {hR n|n ∈ ω} HLR HhLR1 to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove w < SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
Apply HLE w Hw to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
Assume Hwe: w = w0 * y + x * w1 + - w0 * w1.
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Assume Hk0: k0 ∈ ω.
Assume Hk0b: eps_ k0 ≤ x + - w0.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Assume Hk1: k1 ∈ ω.
Assume Hk1b: eps_ k1 ≤ y + - w1.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw01: SNo w0.
Assume Hw02: SNoLev w0 ∈ SNoLev x.
Assume Hw03: w0 < x.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw11: SNo w1.
Assume Hw12: SNoLev w1 ∈ SNoLev y.
Assume Hw13: w1 < y.
We prove the intermediate claim Lek0: SNo (eps_ k0).
An exact proof term for the current goal is SNo_eps_ k0 Hk0.
We prove the intermediate claim Lek1: SNo (eps_ k1).
An exact proof term for the current goal is SNo_eps_ k1 Hk1.
We prove the intermediate claim Lk0k1: k0 + k1 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k0 Hk0 k1 Hk1.
We prove the intermediate claim Lek0k1: SNo (eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_eps_ (k0 + k1) Lk0k1.
We prove the intermediate claim LhLk0k1: SNo (hL (k0 + k1)).
An exact proof term for the current goal is LhL (k0 + k1) Lk0k1.
We prove the intermediate claim Lw0y: SNo (w0 * y).
An exact proof term for the current goal is SNo_mul_SNo w0 y Hw01 Hy1.
We prove the intermediate claim Lxw1: SNo (x * w1).
An exact proof term for the current goal is SNo_mul_SNo x w1 Hx1 Hw11.
We prove the intermediate claim Lw0w1: SNo (w0 * w1).
An exact proof term for the current goal is SNo_mul_SNo w0 w1 Hw01 Hw11.
We prove the intermediate claim Lmw0w1: SNo (- w0 * w1).
An exact proof term for the current goal is SNo_minus_SNo (w0 * w1) Lw0w1.
We prove the intermediate claim Lw0yxw1mw0w1: SNo (w0 * y + x * w1 + - w0 * w1).
An exact proof term for the current goal is SNo_add_SNo_3 (w0 * y) (x * w1) (- w0 * w1) Lw0y Lxw1 Lmw0w1.
rewrite the current goal using Hwe (from left to right).
Apply SNoLeLt_tra (w0 * y + x * w1 + - w0 * w1) (hL (k0 + k1)) (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}) Lw0yxw1mw0w1 LhLk0k1 HhLR2 to the current goal.
We will prove w0 * y + x * w1 + - w0 * w1 ≤ hL (k0 + k1).
Apply SNoLtLe_or (hL (k0 + k1)) (w0 * y + x * w1 + - w0 * w1) LhLk0k1 Lw0yxw1mw0w1 to the current goal.
Assume H1: hL (k0 + k1) < w0 * y + x * w1 + - w0 * w1.
We will prove False.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
Apply SNoLt_tra (x * y) (hL (k0 + k1) + eps_ (k0 + k1)) (x * y) Lxy (SNo_add_SNo (hL (k0 + k1)) (eps_ (k0 + k1)) LhLk0k1 Lek0k1) Lxy (L6 (k0 + k1) Lk0k1) to the current goal.
We will prove hL (k0 + k1) + eps_ (k0 + k1) < x * y.
Apply SNoLtLe_tra (hL (k0 + k1) + eps_ (k0 + k1)) ((w0 * y + x * w1 + - w0 * w1) + eps_ (k0 + k1)) (x * y) (SNo_add_SNo (hL (k0 + k1)) (eps_ (k0 + k1)) LhLk0k1 Lek0k1) (SNo_add_SNo (w0 * y + x * w1 + - w0 * w1) (eps_ (k0 + k1)) Lw0yxw1mw0w1 Lek0k1) Lxy to the current goal.
We will prove hL (k0 + k1) + eps_ (k0 + k1) < (w0 * y + x * w1 + - w0 * w1) + eps_ (k0 + k1).
Apply add_SNo_Lt1 (hL (k0 + k1)) (eps_ (k0 + k1)) (w0 * y + x * w1 + - w0 * w1) LhLk0k1 Lek0k1 Lw0yxw1mw0w1 to the current goal.
An exact proof term for the current goal is H1.
We will prove (w0 * y + x * w1 + - w0 * w1) + eps_ (k0 + k1) ≤ x * y.
rewrite the current goal using add_SNo_com (w0 * y + x * w1 + - w0 * w1) (eps_ (k0 + k1)) Lw0yxw1mw0w1 Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (x * y) (w0 * y + x * w1 + - w0 * w1) (eps_ (k0 + k1)) Lxy Lw0yxw1mw0w1 Lek0k1 to the current goal.
We will prove eps_ (k0 + k1) ≤ x * y + - (w0 * y + x * w1 + - w0 * w1).
rewrite the current goal using add_SNo_com_3_0_1 (w0 * y) (x * w1) (- w0 * w1) Lw0y Lxw1 Lmw0w1 (from left to right).
We will prove eps_ (k0 + k1) ≤ x * y + - (x * w1 + w0 * y + - w0 * w1).
rewrite the current goal using minus_add_SNo_distr_3 (x * w1) (w0 * y) (- w0 * w1) Lxw1 Lw0y Lmw0w1 (from left to right).
We will prove eps_ (k0 + k1) ≤ x * y + - x * w1 + - w0 * y + - - w0 * w1.
rewrite the current goal using mul_SNo_minus_distrL w0 y Hw01 Hy1 (from right to left).
rewrite the current goal using mul_SNo_minus_distrL w0 w1 Hw01 Hw11 (from right to left).
We will prove eps_ (k0 + k1) ≤ x * y + - x * w1 + (- w0) * y + - (- w0) * w1.
rewrite the current goal using mul_SNo_minus_distrR x w1 Hx1 Hw11 (from right to left).
rewrite the current goal using mul_SNo_minus_distrR (- w0) w1 (SNo_minus_SNo w0 Hw01) Hw11 (from right to left).
We will prove eps_ (k0 + k1) ≤ x * y + x * (- w1) + (- w0) * y + (- w0) * (- w1).
rewrite the current goal using SNo_foil x (- w0) y (- w1) Hx1 (SNo_minus_SNo w0 Hw01) Hy1 (SNo_minus_SNo w1 Hw11) (from right to left).
We will prove eps_ (k0 + k1) ≤ (x + - w0) * (y + - w1).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k0 Hk0 k1 Hk1 (from right to left).
We will prove eps_ k0 * eps_ k1 ≤ (x + - w0) * (y + - w1).
Apply nonneg_mul_SNo_Le2 (eps_ k0) (eps_ k1) (x + - w0) (y + - w1) Lek0 Lek1 (SNo_add_SNo x (- w0) Hx1 (SNo_minus_SNo w0 Hw01)) (SNo_add_SNo y (- w1) Hy1 (SNo_minus_SNo w1 Hw11)) to the current goal.
We will prove 0 ≤ eps_ k0.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k0 Hk0.
We will prove 0 ≤ eps_ k1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k1 Hk1.
We will prove eps_ k0 ≤ x + - w0.
An exact proof term for the current goal is Hk0b.
We will prove eps_ k1 ≤ y + - w1.
An exact proof term for the current goal is Hk1b.
Assume H1: w0 * y + x * w1 + - w0 * w1 ≤ hL (k0 + k1).
An exact proof term for the current goal is H1.
We will prove hL (k0 + k1) < SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
An exact proof term for the current goal is HhLR5 (k0 + k1) Lk0k1.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
Assume Hwe: w = z0 * y + x * z1 + - z0 * z1.
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Assume Hk0: k0 ∈ ω.
Assume Hk0b: eps_ k0 ≤ z0 + - x.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Assume Hk1: k1 ∈ ω.
Assume Hk1b: eps_ k1 ≤ z1 + - y.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz01: SNo z0.
Assume Hz02: SNoLev z0 ∈ SNoLev x.
Assume Hz03: x < z0.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz11: SNo z1.
Assume Hz12: SNoLev z1 ∈ SNoLev y.
Assume Hz13: y < z1.
We prove the intermediate claim Lek0: SNo (eps_ k0).
An exact proof term for the current goal is SNo_eps_ k0 Hk0.
We prove the intermediate claim Lek1: SNo (eps_ k1).
An exact proof term for the current goal is SNo_eps_ k1 Hk1.
We prove the intermediate claim Lk0k1: k0 + k1 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k0 Hk0 k1 Hk1.
We prove the intermediate claim Lek0k1: SNo (eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_eps_ (k0 + k1) Lk0k1.
We prove the intermediate claim LhLk0k1: SNo (hL (k0 + k1)).
An exact proof term for the current goal is LhL (k0 + k1) Lk0k1.
We prove the intermediate claim Lz0y: SNo (z0 * y).
An exact proof term for the current goal is SNo_mul_SNo z0 y Hz01 Hy1.
We prove the intermediate claim Lxz1: SNo (x * z1).
An exact proof term for the current goal is SNo_mul_SNo x z1 Hx1 Hz11.
We prove the intermediate claim Lz0z1: SNo (z0 * z1).
An exact proof term for the current goal is SNo_mul_SNo z0 z1 Hz01 Hz11.
We prove the intermediate claim Lmz0z1: SNo (- z0 * z1).
An exact proof term for the current goal is SNo_minus_SNo (z0 * z1) Lz0z1.
We prove the intermediate claim Lz0yxz1mz0z1: SNo (z0 * y + x * z1 + - z0 * z1).
An exact proof term for the current goal is SNo_add_SNo_3 (z0 * y) (x * z1) (- z0 * z1) Lz0y Lxz1 Lmz0z1.
rewrite the current goal using Hwe (from left to right).
Apply SNoLeLt_tra (z0 * y + x * z1 + - z0 * z1) (hL (k0 + k1)) (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}) Lz0yxz1mz0z1 LhLk0k1 HhLR2 to the current goal.
We will prove z0 * y + x * z1 + - z0 * z1 ≤ hL (k0 + k1).
Apply SNoLtLe_or (hL (k0 + k1)) (z0 * y + x * z1 + - z0 * z1) LhLk0k1 Lz0yxz1mz0z1 to the current goal.
Assume H1: hL (k0 + k1) < z0 * y + x * z1 + - z0 * z1.
We will prove False.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
Apply SNoLt_tra (x * y) (hL (k0 + k1) + eps_ (k0 + k1)) (x * y) Lxy (SNo_add_SNo (hL (k0 + k1)) (eps_ (k0 + k1)) LhLk0k1 Lek0k1) Lxy (L6 (k0 + k1) Lk0k1) to the current goal.
We will prove hL (k0 + k1) + eps_ (k0 + k1) < x * y.
Apply SNoLtLe_tra (hL (k0 + k1) + eps_ (k0 + k1)) ((z0 * y + x * z1 + - z0 * z1) + eps_ (k0 + k1)) (x * y) (SNo_add_SNo (hL (k0 + k1)) (eps_ (k0 + k1)) LhLk0k1 Lek0k1) (SNo_add_SNo (z0 * y + x * z1 + - z0 * z1) (eps_ (k0 + k1)) Lz0yxz1mz0z1 Lek0k1) Lxy to the current goal.
We will prove hL (k0 + k1) + eps_ (k0 + k1) < (z0 * y + x * z1 + - z0 * z1) + eps_ (k0 + k1).
Apply add_SNo_Lt1 (hL (k0 + k1)) (eps_ (k0 + k1)) (z0 * y + x * z1 + - z0 * z1) LhLk0k1 Lek0k1 Lz0yxz1mz0z1 to the current goal.
An exact proof term for the current goal is H1.
We will prove (z0 * y + x * z1 + - z0 * z1) + eps_ (k0 + k1) ≤ x * y.
rewrite the current goal using add_SNo_com (z0 * y + x * z1 + - z0 * z1) (eps_ (k0 + k1)) Lz0yxz1mz0z1 Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (x * y) (z0 * y + x * z1 + - z0 * z1) (eps_ (k0 + k1)) Lxy Lz0yxz1mz0z1 Lek0k1 to the current goal.
We will prove eps_ (k0 + k1) ≤ x * y + - (z0 * y + x * z1 + - z0 * z1).
rewrite the current goal using add_SNo_com (x * y) (- (z0 * y + x * z1 + - z0 * z1)) Lxy (SNo_minus_SNo (z0 * y + x * z1 + - z0 * z1) Lz0yxz1mz0z1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (z0 * y) (x * z1) (- z0 * z1) Lz0y Lxz1 Lmz0z1 (from left to right).
rewrite the current goal using minus_add_SNo_distr_3 (- z0 * z1) (z0 * y) (x * z1) Lmz0z1 Lz0y Lxz1 (from left to right).
rewrite the current goal using minus_SNo_invol (z0 * z1) Lz0z1 (from left to right).
We will prove eps_ (k0 + k1) ≤ (z0 * z1 + - z0 * y + - x * z1) + x * y.
rewrite the current goal using add_SNo_assoc_4 (z0 * z1) (- z0 * y) (- x * z1) (x * y) Lz0z1 (SNo_minus_SNo (z0 * y) Lz0y) (SNo_minus_SNo (x * z1) Lxz1) Lxy (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * z1 + - z0 * y + - x * z1 + x * y.
rewrite the current goal using mul_SNo_minus_distrR z0 y Hz01 Hy1 (from right to left).
rewrite the current goal using mul_SNo_minus_distrL x z1 Hx1 Hz11 (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * z1 + z0 * (- y) + (- x) * z1 + x * y.
rewrite the current goal using mul_SNo_minus_minus x y Hx1 Hy1 (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * z1 + z0 * (- y) + (- x) * z1 + (- x) * (- y).
rewrite the current goal using SNo_foil z0 (- x) z1 (- y) Hz01 (SNo_minus_SNo x Hx1) Hz11 (SNo_minus_SNo y Hy1) (from right to left).
We will prove eps_ (k0 + k1) ≤ (z0 + - x) * (z1 + - y).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k0 Hk0 k1 Hk1 (from right to left).
We will prove eps_ k0 * eps_ k1 ≤ (z0 + - x) * (z1 + - y).
Apply nonneg_mul_SNo_Le2 (eps_ k0) (eps_ k1) (z0 + - x) (z1 + - y) Lek0 Lek1 (SNo_add_SNo z0 (- x) Hz01 (SNo_minus_SNo x Hx1)) (SNo_add_SNo z1 (- y) Hz11 (SNo_minus_SNo y Hy1)) to the current goal.
We will prove 0 ≤ eps_ k0.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k0 Hk0.
We will prove 0 ≤ eps_ k1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k1 Hk1.
We will prove eps_ k0 ≤ z0 + - x.
An exact proof term for the current goal is Hk0b.
We will prove eps_ k1 ≤ z1 + - y.
An exact proof term for the current goal is Hk1b.
Assume H1: z0 * y + x * z1 + - z0 * z1 ≤ hL (k0 + k1).
An exact proof term for the current goal is H1.
We will prove hL (k0 + k1) < SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
An exact proof term for the current goal is HhLR5 (k0 + k1) Lk0k1.
Let z be given.
Assume Hz: z ∈ R.
We will prove SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω} < z.
Apply HRE z Hz to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
Assume Hze: z = w0 * y + x * z1 + - w0 * z1.
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Assume Hk0: k0 ∈ ω.
Assume Hk0b: eps_ k0 ≤ x + - w0.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Assume Hk1: k1 ∈ ω.
Assume Hk1b: eps_ k1 ≤ z1 + - y.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw01: SNo w0.
Assume Hw02: SNoLev w0 ∈ SNoLev x.
Assume Hw03: w0 < x.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz11: SNo z1.
Assume Hz12: SNoLev z1 ∈ SNoLev y.
Assume Hz13: y < z1.
We prove the intermediate claim Lek0: SNo (eps_ k0).
An exact proof term for the current goal is SNo_eps_ k0 Hk0.
We prove the intermediate claim Lek1: SNo (eps_ k1).
An exact proof term for the current goal is SNo_eps_ k1 Hk1.
We prove the intermediate claim Lk0k1: k0 + k1 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k0 Hk0 k1 Hk1.
We prove the intermediate claim Lek0k1: SNo (eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_eps_ (k0 + k1) Lk0k1.
We prove the intermediate claim Lmek0k1: SNo (- eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_minus_SNo (eps_ (k0 + k1)) Lek0k1.
We prove the intermediate claim LhRk0k1: SNo (hR (k0 + k1)).
An exact proof term for the current goal is LhR (k0 + k1) Lk0k1.
We prove the intermediate claim Lw0y: SNo (w0 * y).
An exact proof term for the current goal is SNo_mul_SNo w0 y Hw01 Hy1.
We prove the intermediate claim Lxz1: SNo (x * z1).
An exact proof term for the current goal is SNo_mul_SNo x z1 Hx1 Hz11.
We prove the intermediate claim Lw0z1: SNo (w0 * z1).
An exact proof term for the current goal is SNo_mul_SNo w0 z1 Hw01 Hz11.
We prove the intermediate claim Lmw0z1: SNo (- w0 * z1).
An exact proof term for the current goal is SNo_minus_SNo (w0 * z1) Lw0z1.
We prove the intermediate claim Lw0yxz1mw0z1: SNo (w0 * y + x * z1 + - w0 * z1).
An exact proof term for the current goal is SNo_add_SNo_3 (w0 * y) (x * z1) (- w0 * z1) Lw0y Lxz1 Lmw0z1.
rewrite the current goal using Hze (from left to right).
Apply SNoLtLe_tra (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}) (hR (k0 + k1)) (w0 * y + x * z1 + - w0 * z1) HhLR2 LhRk0k1 Lw0yxz1mw0z1 to the current goal.
We will prove SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω} < hR (k0 + k1).
An exact proof term for the current goal is HhLR6 (k0 + k1) Lk0k1.
We will prove hR (k0 + k1) ≤ w0 * y + x * z1 + - w0 * z1.
Apply SNoLtLe_or (w0 * y + x * z1 + - w0 * z1) (hR (k0 + k1)) Lw0yxz1mw0z1 LhRk0k1 to the current goal.
Assume H1: w0 * y + x * z1 + - w0 * z1 < hR (k0 + k1).
We will prove False.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
Apply SNoLt_tra (x * y) (hR (k0 + k1) + - eps_ (k0 + k1)) (x * y) Lxy (SNo_add_SNo (hR (k0 + k1)) (- eps_ (k0 + k1)) LhRk0k1 Lmek0k1) Lxy to the current goal.
We will prove x * y < hR (k0 + k1) + - eps_ (k0 + k1).
Apply SNoLeLt_tra (x * y) ((w0 * y + x * z1 + - w0 * z1) + - eps_ (k0 + k1)) (hR (k0 + k1) + - eps_ (k0 + k1)) Lxy (SNo_add_SNo (w0 * y + x * z1 + - w0 * z1) (- eps_ (k0 + k1)) Lw0yxz1mw0z1 Lmek0k1) (SNo_add_SNo (hR (k0 + k1)) (- eps_ (k0 + k1)) LhRk0k1 Lmek0k1) to the current goal.
We will prove x * y ≤ (w0 * y + x * z1 + - w0 * z1) + - eps_ (k0 + k1).
Apply add_SNo_minus_Le2b (w0 * y + x * z1 + - w0 * z1) (eps_ (k0 + k1)) (x * y) Lw0yxz1mw0z1 Lek0k1 Lxy to the current goal.
We will prove x * y + eps_ (k0 + k1) ≤ w0 * y + x * z1 + - w0 * z1.
rewrite the current goal using add_SNo_com (x * y) (eps_ (k0 + k1)) Lxy Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (w0 * y + x * z1 + - w0 * z1) (x * y) (eps_ (k0 + k1)) Lw0yxz1mw0z1 Lxy Lek0k1 to the current goal.
We will prove eps_ (k0 + k1) ≤ (w0 * y + x * z1 + - w0 * z1) + - x * y.
rewrite the current goal using add_SNo_rotate_3_1 (w0 * y) (x * z1) (- w0 * z1) Lw0y Lxz1 Lmw0z1 (from left to right).
We will prove eps_ (k0 + k1) ≤ (- w0 * z1 + w0 * y + x * z1) + - x * y.
rewrite the current goal using add_SNo_assoc_4 (- w0 * z1) (w0 * y) (x * z1) (- x * y) Lmw0z1 Lw0y Lxz1 Lmxy (from right to left).
We will prove eps_ (k0 + k1) ≤ - w0 * z1 + w0 * y + x * z1 + - x * y.
rewrite the current goal using add_SNo_rotate_4_1 (- w0 * z1) (w0 * y) (x * z1) (- x * y) Lmw0z1 Lw0y Lxz1 Lmxy (from left to right).
We will prove eps_ (k0 + k1) ≤ - x * y + - w0 * z1 + w0 * y + x * z1.
rewrite the current goal using add_SNo_rotate_4_1 (- x * y) (- w0 * z1) (w0 * y) (x * z1) Lmxy Lmw0z1 Lw0y Lxz1 (from left to right).
We will prove eps_ (k0 + k1) ≤ x * z1 + - x * y + - w0 * z1 + w0 * y.
rewrite the current goal using mul_SNo_minus_distrR x y Hx1 Hy1 (from right to left).
rewrite the current goal using mul_SNo_minus_distrL w0 z1 Hw01 Hz11 (from right to left).
rewrite the current goal using mul_SNo_minus_minus w0 y Hw01 Hy1 (from right to left).
We will prove eps_ (k0 + k1) ≤ x * z1 + x * (- y) + (- w0) * z1 + (- w0) * (- y).
rewrite the current goal using SNo_foil x (- w0) z1 (- y) Hx1 (SNo_minus_SNo w0 Hw01) Hz11 (SNo_minus_SNo y Hy1) (from right to left).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k0 Hk0 k1 Hk1 (from right to left).
We will prove eps_ k0 * eps_ k1 ≤ (x + - w0) * (z1 + - y).
Apply nonneg_mul_SNo_Le2 (eps_ k0) (eps_ k1) (x + - w0) (z1 + - y) Lek0 Lek1 (SNo_add_SNo x (- w0) Hx1 (SNo_minus_SNo w0 Hw01)) (SNo_add_SNo z1 (- y) Hz11 (SNo_minus_SNo y Hy1)) to the current goal.
We will prove 0 ≤ eps_ k0.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k0 Hk0.
We will prove 0 ≤ eps_ k1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k1 Hk1.
We will prove eps_ k0 ≤ x + - w0.
An exact proof term for the current goal is Hk0b.
We will prove eps_ k1 ≤ z1 + - y.
An exact proof term for the current goal is Hk1b.
We will prove (w0 * y + x * z1 + - w0 * z1) + - eps_ (k0 + k1) < hR (k0 + k1) + - eps_ (k0 + k1).
Apply add_SNo_Lt1 (w0 * y + x * z1 + - w0 * z1) (- eps_ (k0 + k1)) (hR (k0 + k1)) Lw0yxz1mw0z1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is L8 (k0 + k1) Lk0k1.
Assume H1: hR (k0 + k1) ≤ w0 * y + x * z1 + - w0 * z1.
An exact proof term for the current goal is H1.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
Assume Hze: z = z0 * y + x * w1 + - z0 * w1.
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Assume Hk0: k0 ∈ ω.
Assume Hk0b: eps_ k0 ≤ z0 + - x.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Assume Hk1: k1 ∈ ω.
Assume Hk1b: eps_ k1 ≤ y + - w1.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz01: SNo z0.
Assume Hz02: SNoLev z0 ∈ SNoLev x.
Assume Hz03: x < z0.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw11: SNo w1.
Assume Hw12: SNoLev w1 ∈ SNoLev y.
Assume Hw13: w1 < y.
We prove the intermediate claim Lek0: SNo (eps_ k0).
An exact proof term for the current goal is SNo_eps_ k0 Hk0.
We prove the intermediate claim Lek1: SNo (eps_ k1).
An exact proof term for the current goal is SNo_eps_ k1 Hk1.
We prove the intermediate claim Lk0k1: k0 + k1 ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k0 Hk0 k1 Hk1.
We prove the intermediate claim Lek0k1: SNo (eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_eps_ (k0 + k1) Lk0k1.
We prove the intermediate claim Lmek0k1: SNo (- eps_ (k0 + k1)).
An exact proof term for the current goal is SNo_minus_SNo (eps_ (k0 + k1)) Lek0k1.
We prove the intermediate claim LhRk0k1: SNo (hR (k0 + k1)).
An exact proof term for the current goal is LhR (k0 + k1) Lk0k1.
We prove the intermediate claim Lz0y: SNo (z0 * y).
An exact proof term for the current goal is SNo_mul_SNo z0 y Hz01 Hy1.
We prove the intermediate claim Lxw1: SNo (x * w1).
An exact proof term for the current goal is SNo_mul_SNo x w1 Hx1 Hw11.
We prove the intermediate claim Lz0w1: SNo (z0 * w1).
An exact proof term for the current goal is SNo_mul_SNo z0 w1 Hz01 Hw11.
We prove the intermediate claim Lmz0w1: SNo (- z0 * w1).
An exact proof term for the current goal is SNo_minus_SNo (z0 * w1) Lz0w1.
We prove the intermediate claim Lz0yxw1mz0w1: SNo (z0 * y + x * w1 + - z0 * w1).
An exact proof term for the current goal is SNo_add_SNo_3 (z0 * y) (x * w1) (- z0 * w1) Lz0y Lxw1 Lmz0w1.
rewrite the current goal using Hze (from left to right).
Apply SNoLtLe_tra (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}) (hR (k0 + k1)) (z0 * y + x * w1 + - z0 * w1) HhLR2 LhRk0k1 Lz0yxw1mz0w1 to the current goal.
We will prove SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω} < hR (k0 + k1).
An exact proof term for the current goal is HhLR6 (k0 + k1) Lk0k1.
We will prove hR (k0 + k1) ≤ z0 * y + x * w1 + - z0 * w1.
Apply SNoLtLe_or (z0 * y + x * w1 + - z0 * w1) (hR (k0 + k1)) Lz0yxw1mz0w1 LhRk0k1 to the current goal.
Assume H1: z0 * y + x * w1 + - z0 * w1 < hR (k0 + k1).
We will prove False.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
Apply SNoLt_tra (x * y) (hR (k0 + k1) + - eps_ (k0 + k1)) (x * y) Lxy (SNo_add_SNo (hR (k0 + k1)) (- eps_ (k0 + k1)) LhRk0k1 Lmek0k1) Lxy to the current goal.
We will prove x * y < hR (k0 + k1) + - eps_ (k0 + k1).
Apply SNoLeLt_tra (x * y) ((z0 * y + x * w1 + - z0 * w1) + - eps_ (k0 + k1)) (hR (k0 + k1) + - eps_ (k0 + k1)) Lxy (SNo_add_SNo (z0 * y + x * w1 + - z0 * w1) (- eps_ (k0 + k1)) Lz0yxw1mz0w1 Lmek0k1) (SNo_add_SNo (hR (k0 + k1)) (- eps_ (k0 + k1)) LhRk0k1 Lmek0k1) to the current goal.
We will prove x * y ≤ (z0 * y + x * w1 + - z0 * w1) + - eps_ (k0 + k1).
Apply add_SNo_minus_Le2b (z0 * y + x * w1 + - z0 * w1) (eps_ (k0 + k1)) (x * y) Lz0yxw1mz0w1 Lek0k1 Lxy to the current goal.
We will prove x * y + eps_ (k0 + k1) ≤ z0 * y + x * w1 + - z0 * w1.
rewrite the current goal using add_SNo_com (x * y) (eps_ (k0 + k1)) Lxy Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (z0 * y + x * w1 + - z0 * w1) (x * y) (eps_ (k0 + k1)) Lz0yxw1mz0w1 Lxy Lek0k1 to the current goal.
We will prove eps_ (k0 + k1) ≤ (z0 * y + x * w1 + - z0 * w1) + - x * y.
rewrite the current goal using add_SNo_assoc_4 (z0 * y) (x * w1) (- z0 * w1) (- x * y) Lz0y Lxw1 Lmz0w1 Lmxy (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * y + x * w1 + - z0 * w1 + - x * y.
rewrite the current goal using add_SNo_rotate_3_1 (- z0 * w1) (- x * y) (x * w1) Lmz0w1 Lmxy Lxw1 (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * y + - z0 * w1 + - x * y + x * w1.
rewrite the current goal using mul_SNo_minus_distrR z0 w1 Hz01 Hw11 (from right to left).
rewrite the current goal using mul_SNo_minus_distrL x y Hx1 Hy1 (from right to left).
rewrite the current goal using mul_SNo_minus_minus x w1 Hx1 Hw11 (from right to left).
We will prove eps_ (k0 + k1) ≤ z0 * y + z0 * (- w1) + (- x) * y + (- x) * (- w1).
rewrite the current goal using SNo_foil z0 (- x) y (- w1) Hz01 (SNo_minus_SNo x Hx1) Hy1 (SNo_minus_SNo w1 Hw11) (from right to left).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k0 Hk0 k1 Hk1 (from right to left).
We will prove eps_ k0 * eps_ k1 ≤ (z0 + - x) * (y + - w1).
Apply nonneg_mul_SNo_Le2 (eps_ k0) (eps_ k1) (z0 + - x) (y + - w1) Lek0 Lek1 (SNo_add_SNo z0 (- x) Hz01 (SNo_minus_SNo x Hx1)) (SNo_add_SNo y (- w1) Hy1 (SNo_minus_SNo w1 Hw11)) to the current goal.
We will prove 0 ≤ eps_ k0.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k0 Hk0.
We will prove 0 ≤ eps_ k1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos k1 Hk1.
We will prove eps_ k0 ≤ z0 + - x.
An exact proof term for the current goal is Hk0b.
We will prove eps_ k1 ≤ y + - w1.
An exact proof term for the current goal is Hk1b.
We will prove (z0 * y + x * w1 + - z0 * w1) + - eps_ (k0 + k1) < hR (k0 + k1) + - eps_ (k0 + k1).
Apply add_SNo_Lt1 (z0 * y + x * w1 + - z0 * w1) (- eps_ (k0 + k1)) (hR (k0 + k1)) Lz0yxw1mz0w1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is L8 (k0 + k1) Lk0k1.
Assume H1: hR (k0 + k1) ≤ z0 * y + x * w1 + - z0 * w1.
An exact proof term for the current goal is H1.
Let w be given.
Assume Hw: w ∈ {hL n|n ∈ ω}.
rewrite the current goal using HxyLR (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 Hwn.
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 ∈ {hR n|n ∈ ω}.
rewrite the current goal using HxyLR (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 Hzn.
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 L4 n Hn.
Apply HC to the current goal.
An exact proof term for the current goal is SNo_approx_real (x * y) Lxy hL HhL1 hR HhR1 L3 L6 L7 L4 L9 L10.
∎