Proof:Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hx0 Hy0.
Apply dneg to the current goal.
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.
We prove the intermediate
claim Ly7:
∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < y → y < q + eps_ k → p) → p.
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) ∉ ω.
Apply HC 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.
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.
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 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.
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 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.
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 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.
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 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.
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.
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.
rewrite the current goal using Hx6 v (LLx v Hv) H1 (from right to left) at position 1.
An exact proof term for the current goal is Hv3.
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
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.
An exact proof term for the current goal is H3.
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.
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.
rewrite the current goal using Hx6 v (LRx v Hv) H1 (from right to left) at position 2.
An exact proof term for the current goal is Hv3.
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
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.
An exact proof term for the current goal is H3.
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.
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.
rewrite the current goal using Hy6 v (LLy v Hv) H1 (from right to left) at position 1.
An exact proof term for the current goal is Hv3.
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
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.
An exact proof term for the current goal is H3.
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.
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.
rewrite the current goal using Hy6 v (LRy v Hv) H1 (from right to left) at position 2.
An exact proof term for the current goal is Hv3.
Apply dneg to the current goal.
Assume H2: ¬ p.
Apply H1 to the current goal.
Let k be given.
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.
An exact proof term for the current goal is H3.
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.
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.
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.
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.
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.
Let w be given.
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 _ _.
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.
Apply LLy2 w Hw to the current goal.
Let k' be given.
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.
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.
Let w be given.
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 _ _.
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.
Apply LRy2 w Hw to the current goal.
Let k' be given.
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.
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.
An exact proof term for the current goal is H1.
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.
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.
Let w be given.
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 _ _.
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.
Apply LRy2 w Hw to the current goal.
Let k' be given.
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).
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.
Let w be given.
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 _ _.
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.
Apply LLy2 w Hw to the current goal.
Let k' be given.
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).
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.
Let N be given.
Assume HN.
Apply HN to the current goal.
Let N' be given.
Assume HN'.
Apply HN' to the current goal.
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.
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.
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 HN.
Apply HN to the current goal.
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.
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.
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.
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.
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.
An exact proof term for the current goal is SNoLt_1_2.
Let hL be given.
Assume HhL.
Apply HhL to the current goal.
Let hR be given.
Assume HhR.
Apply HhR to the current goal.
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.
Assume HhLR1: SNoCutP {hL n|n ∈ ω} {hR n|n ∈ ω}.
Assume HhLR2: SNo (SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}).
Assume _ _.
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.
We will
prove w < SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω}.
Apply HLE w Hw to the current goal.
Let w0 be given.
Let w1 be given.
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw01: SNo w0.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw11: SNo w1.
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.
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.
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.
Let z1 be given.
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz01: SNo z0.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz11: SNo 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.
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.
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.
We will
prove SNoCut {hL n|n ∈ ω} {hR n|n ∈ ω} < z.
Apply HRE z Hz to the current goal.
Let w0 be given.
Let z1 be given.
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw01: SNo w0.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz11: SNo 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.
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.
An exact proof term for the current goal is H1.
Let z0 be given.
Let w1 be given.
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz01: SNo z0.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw11: SNo w1.
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.
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.
An exact proof term for the current goal is H1.
Let w be given.
rewrite the current goal using HxyLR (from right to left).
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.
rewrite the current goal using HxyLR (from right to left).
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.
∎