Let x be given.
Assume Hx Hxnonneg IH HLR.
Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
Set y to be the term
SNoCut L R.
Apply HLR to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
We prove the intermediate
claim Lyy:
SNo (y * y).
An
exact proof term for the current goal is
SNo_mul_SNo y y H1 H1.
We prove the intermediate
claim Lyynn:
0 ≤ y * y.
We prove the intermediate
claim LL_mon:
∀k k', nat_p k → nat_p k' → k ⊆ k' → L_ k ⊆ L_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim LR_mon:
∀k k', nat_p k → nat_p k' → k ⊆ k' → R_ k ⊆ R_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate
claim L1L:
∀w ∈ L, ∀p : prop, (SNo w → 0 ≤ w → w * w < x → p) → p.
Let w be given.
Assume Hw.
Let p be given.
Assume Hp.
Let k be given.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H3.
Apply H3 to the current goal.
An exact proof term for the current goal is Hp.
We prove the intermediate
claim L1R:
∀z ∈ R, ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p.
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Let k be given.
Assume _ H2.
Apply H2 z H1 to the current goal.
Assume H3.
Apply H3 to the current goal.
An exact proof term for the current goal is Hp.
Apply SNoLtE x (y * y) Hx Lyy H6 to the current goal.
Let u be given.
We prove the intermediate
claim Lunn:
0 ≤ u.
An
exact proof term for the current goal is
SNoLeLt_tra 0 x u SNo_0 Hx Hu1 Hxnonneg Hu5.
Apply SNoS_I2 u x Hu1 Hx to the current goal.
Apply IH u LuSx Lunn to the current goal.
Assume H.
Apply H to the current goal.
Apply H4 to the current goal.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
Apply SNoR_I x Hx u Hu1 to the current goal.
An exact proof term for the current goal is Hu5.
Apply SNoLtLe_tra u (y * y) u Hu1 Lyy Hu1 Hu6 to the current goal.
rewrite the current goal using H9 (from right to left).
We prove the intermediate
claim L10:
x ∈ SNoL (y * y).
An
exact proof term for the current goal is
SNoL_I (y * y) Lyy x Hx H7 H6.
Let v be given.
Let w be given.
Apply L1L v Hv to the current goal.
Apply L1L w Hw to the current goal.
We prove the intermediate
claim L11:
∃k, nat_p k ∧ v ∈ L_ k ∧ w ∈ L_ k.
Let k' be given.
Assume H.
Apply H to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
We use k'' to witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k'' Hk''1.
We will
prove v ∈ L_ k''.
An
exact proof term for the current goal is
LL_mon k' k'' (omega_nat_p k' Hk'1) (omega_nat_p k'' Hk''1) H1 v Hk'2.
An exact proof term for the current goal is Hk''2.
We use k' to witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k' Hk'1.
An exact proof term for the current goal is Hk'2.
An
exact proof term for the current goal is
LL_mon k'' k' (omega_nat_p k'' Hk''1) (omega_nat_p k' Hk'1) H1 w Hk''2.
Apply L11 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim Lvw0:
v + w ≠ 0.
Assume H.
rewrite the current goal using H (from right to left) at position 2.
An exact proof term for the current goal is H11.
We prove the intermediate
claim L12:
(x + v * w) :/: (v + w) ∈ R_ (ordsucc k).
rewrite the current goal using
tuple_2_1_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (L_ k) (L_ k) x v Hvk w Hwk H11.
We prove the intermediate
claim L13:
(x + v * w) :/: (v + w) ∈ R.
We prove the intermediate
claim L14:
y < (x + v * w) :/: (v + w).
An
exact proof term for the current goal is
H4 ((x + v * w) :/: (v + w)) L13.
We prove the intermediate
claim L15:
v * y + y * w = y * (v + w).
Use transitivity with and
y * v + y * w.
Use f_equal.
We will
prove v * y = y * v.
An
exact proof term for the current goal is
mul_SNo_com v y Hv1 H1.
We will
prove y * v + y * w = y * (v + w).
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_distrL y v w H1 Hv1 Hw1.
We will
prove v * y + y * w < x + v * w.
rewrite the current goal using L15 (from left to right).
We will
prove y * (v + w) < x + v * w.
We will
prove y * (v + w) < ((x + v * w) :/: (v + w)) * (v + w).
We prove the intermediate
claim L16:
v = 0 ∧ w = 0.
rewrite the current goal using
add_SNo_0R v Hv1 (from right to left) at position 1.
We will
prove v + 0 ≤ v + w.
An exact proof term for the current goal is H11.
rewrite the current goal using
add_SNo_0L w Hw1 (from right to left) at position 1.
We will
prove 0 + w ≤ v + w.
An exact proof term for the current goal is H11.
Apply andI to the current goal.
Apply L16 to the current goal.
We prove the intermediate
claim L17:
x + v * w = x.
rewrite the current goal using Hv0 (from left to right).
rewrite the current goal using
mul_SNo_zeroL w Hw1 (from left to right).
An
exact proof term for the current goal is
add_SNo_0R x Hx.
We prove the intermediate
claim L18:
v * y + y * w = 0.
rewrite the current goal using Hv0 (from left to right).
We will
prove 0 * y + y * w = 0.
rewrite the current goal using Hw0 (from left to right).
We prove the intermediate
claim L19:
x ≤ 0.
rewrite the current goal using L17 (from right to left).
rewrite the current goal using L18 (from right to left).
An exact proof term for the current goal is H10.
We prove the intermediate
claim L20:
x = 0.
We will
prove v * v < v * v.
rewrite the current goal using Hv0 (from left to right) at position 3.
We will
prove v * v < 0 * v.
rewrite the current goal using
mul_SNo_zeroL v Hv1 (from left to right).
rewrite the current goal using L20 (from right to left).
An exact proof term for the current goal is Hv3.
Let v be given.
Let w be given.
Apply L1R v Hv to the current goal.
Apply L1R w Hw to the current goal.
We prove the intermediate
claim L21:
∃k, nat_p k ∧ v ∈ R_ k ∧ w ∈ R_ k.
Let k' be given.
Assume H.
Apply H to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
We use k'' to witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k'' Hk''1.
We will
prove v ∈ R_ k''.
An
exact proof term for the current goal is
LR_mon k' k'' (omega_nat_p k' Hk'1) (omega_nat_p k'' Hk''1) H1 v Hk'2.
An exact proof term for the current goal is Hk''2.
We use k' to witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k' Hk'1.
An exact proof term for the current goal is Hk'2.
An
exact proof term for the current goal is
LR_mon k'' k' (omega_nat_p k'' Hk''1) (omega_nat_p k' Hk'1) H1 w Hk''2.
Apply L21 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim Lvwpos:
0 < v + w.
rewrite the current goal using
add_SNo_0R v Hv1 (from right to left) at position 1.
We will
prove v + 0 < v + w.
Apply H4 to the current goal.
We prove the intermediate
claim Lvw0:
v + w ≠ 0.
Assume H.
rewrite the current goal using H (from right to left) at position 2.
An exact proof term for the current goal is Lvwpos.
We prove the intermediate
claim L22:
(x + v * w) :/: (v + w) ∈ R_ (ordsucc k).
rewrite the current goal using
tuple_2_1_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (R_ k) (R_ k) x v Hvk w Hwk Lvwpos.
We prove the intermediate
claim L23:
(x + v * w) :/: (v + w) ∈ R.
We prove the intermediate
claim L24:
y < (x + v * w) :/: (v + w).
An
exact proof term for the current goal is
H4 ((x + v * w) :/: (v + w)) L23.
We prove the intermediate
claim L25:
v * y + y * w = y * (v + w).
Use transitivity with and
y * v + y * w.
Use f_equal.
We will
prove v * y = y * v.
An
exact proof term for the current goal is
mul_SNo_com v y Hv1 H1.
We will
prove y * v + y * w = y * (v + w).
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_distrL y v w H1 Hv1 Hw1.
We will
prove v * y + y * w < x + v * w.
rewrite the current goal using L25 (from left to right).
We will
prove y * (v + w) < x + v * w.
We will
prove y * (v + w) < ((x + v * w) :/: (v + w)) * (v + w).
Apply IH (y * y) (SNoS_I2 (y * y) x Lyy Hx H7) Lyynn to the current goal.
Assume H.
Apply H to the current goal.
rewrite the current goal using Lsryy (from right to left) at position 2.
Apply H4 to the current goal.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
An
exact proof term for the current goal is
SNoR_I x Hx (y * y) Lyy H7 H6.
∎