Let x be given.
Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
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.
We prove the intermediate
claim L2:
SNoCutP L R.
Apply L2 to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
Set y to be the term
SNoCut L R.
We prove the intermediate
claim Lynn:
0 ≤ y.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Lynn.
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.
An exact proof term for the current goal is H6.
∎