Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
Let k be given.
Assume Hk.
Let w be given.
Assume Hw.
Let k be given.
Assume Hk.
Let z be given.
Assume Hz.
Let w be given.
Let p be given.
Assume Hp.
Let k be given.
An exact proof term for the current goal is Hp k Hk Hwk.
Let z be given.
Let p be given.
Assume Hp.
Let k be given.
An exact proof term for the current goal is Hp k Hk Hzk.
We prove the intermediate
claim L_L_Subq:
∀k, nat_p k → L_ k ⊆ L_ (ordsucc k).
Let k be given.
Assume Hk.
Let w be given.
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is Hw.
We prove the intermediate
claim L_R_Subq:
∀k, nat_p k → R_ k ⊆ R_ (ordsucc k).
Let k be given.
Assume Hk.
Let w be given.
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is Hw.
We prove the intermediate
claim L_L_R_Subq:
∀k, nat_p k → ∀k' ∈ k, L_ k' ⊆ L_ k ∧ R_ k' ⊆ R_ k.
Let k' be given.
An
exact proof term for the current goal is
EmptyE k' Hk'.
Let k be given.
Assume Hk.
Let k' be given.
Apply ordsuccE k k' Hk' to the current goal.
Apply IHk k' Hk'2 to the current goal.
Assume IHkL IHkR.
Apply andI to the current goal.
An exact proof term for the current goal is L_L_Subq k Hk.
An exact proof term for the current goal is L_R_Subq k Hk.
rewrite the current goal using Hk'2 (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is L_L_Subq k Hk.
An exact proof term for the current goal is L_R_Subq k Hk.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
Let w' be given.
Assume Hw'.
Let w be given.
rewrite the current goal using Hw'w (from left to right).
Apply SepE (SNoL x) (λw ⇒ 0 ≤ w) w Hw to the current goal.
Apply SNoL_E x Hx1 w Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c.
Apply SepI to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hw1b.
An exact proof term for the current goal is Hw1a.
An exact proof term for the current goal is Hwnneg.
Let z' be given.
Assume Hz'.
Let z be given.
rewrite the current goal using Hz'z (from left to right).
Apply SNoR_E x Hx1 z Hz to the current goal.
Assume Hz1 Hz2 Hz3.
Apply SepI to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hz2.
An exact proof term for the current goal is Hz1.
An
exact proof term for the current goal is
SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3.
An
exact proof term for the current goal is
SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
We prove the intermediate
claim LLsR:
L ⊆ real.
Let w be given.
Assume Hw.
Apply LLE w Hw to the current goal.
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume H _.
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w) w (H w Hwk).
We prove the intermediate
claim LRsR:
R ⊆ real.
Let z be given.
Assume Hz.
Apply LRE z Hz to the current goal.
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume _ H.
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w) z (H z Hzk).
We prove the intermediate
claim LLR:
SNoCutP L R.
Assume HLR1 HLR2.
Assume HLR5.
We prove the intermediate
claim L0Lx:
0 ∈ SNoLev x.
rewrite the current goal using H4 (from left to right).
We prove the intermediate
claim L1Lx:
1 ∈ SNoLev x.
rewrite the current goal using H4 (from left to right).
We prove the intermediate
claim LLne:
L ≠ 0.
We prove the intermediate
claim LRne:
R ≠ 0.
We prove the intermediate
claim LRE':
∀z ∈ R, SNo z ∧ 0 < z.
Let z be given.
Assume Hz.
We prove the intermediate
claim LzS:
SNo z.
An
exact proof term for the current goal is
real_SNo z (LRsR z Hz).
Apply andI to the current goal.
An exact proof term for the current goal is LzS.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is HLR4 z Hz.
We prove the intermediate
claim LLnomax:
∀w ∈ L, ∃w' ∈ L, w < w'.
Let w be given.
Assume Hw.
Apply LLE w Hw to the current goal.
Let k be given.
Assume Hk.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume H _.
Apply SepE real (λw ⇒ 0 ≤ w) w (H w Hwk) to the current goal.
We prove the intermediate
claim Lw:
SNo w.
An
exact proof term for the current goal is
real_SNo w HwR.
Apply xm (∃z, z ∈ R) to the current goal.
Assume H5.
Apply H5 to the current goal.
Let z be given.
Apply LRE z Hz to the current goal.
Let k' be given.
Assume Hk'.
Apply LRE' z Hz to the current goal.
Apply L_L_R_real k' (omega_nat_p k' Hk') to the current goal.
Assume _ H.
We prove the intermediate
claim LzR:
z ∈ real.
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w) z (H z Hzk').
We prove the intermediate
claim Lz:
SNo z.
An
exact proof term for the current goal is
real_SNo z LzR.
We prove the intermediate
claim Lzpos:
0 < z.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is HLR4 z Hz.
We prove the intermediate
claim Lwz:
SNo (w + z).
An
exact proof term for the current goal is
SNo_add_SNo w z Lw Lz.
We prove the intermediate
claim Lwmz:
SNo (w * z).
An
exact proof term for the current goal is
SNo_mul_SNo w z Lw Lz.
We prove the intermediate
claim Lwzpos:
0 < w + z.
An exact proof term for the current goal is Lzpos.
Set w' to be the term
(x + w * z) :/: (w + z).
We use w' to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate
claim Lwzk'':
∃k'' ∈ ω, w ∈ L_ k'' ∧ z ∈ R_ k''.
We use k' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk'.
Apply andI to the current goal.
Apply L_L_R_Subq k' (omega_nat_p k' Hk') k H6 to the current goal.
Assume H _.
An exact proof term for the current goal is H w Hwk.
An exact proof term for the current goal is Hzk'.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
Apply andI to the current goal.
An exact proof term for the current goal is Hwk.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hzk'.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
Apply andI to the current goal.
An exact proof term for the current goal is Hwk.
Apply L_L_R_Subq k (omega_nat_p k Hk) k' H6 to the current goal.
Assume _ H.
An exact proof term for the current goal is H z Hzk'.
Apply Lwzk'' 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 Lw'LSk'':
w' ∈ L_ (ordsucc k'').
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is Hwk''.
An exact proof term for the current goal is Hzk''.
An exact proof term for the current goal is Lwzpos.
We will
prove w < (x + w * z) :/: (w + z).
We will
prove w * (w + z) < x + w * z.
rewrite the current goal using
mul_SNo_distrL w w z Lw Lw HzS (from left to right).
We will
prove w * w + w * z < x + w * z.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is HLR3 w Hw.
rewrite the current goal using H6 (from right to left).
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Lwsx.
Apply LRne to the current goal.
Let z be given.
Assume Hz.
Apply H5 to the current goal.
We use z to witness the existential quantifier.
An exact proof term for the current goal is Hz.
We prove the intermediate
claim LRnomin:
∀z ∈ R, ∃z' ∈ R, z' < z.
Let z be given.
Assume Hz.
Apply LRE z Hz to the current goal.
Let k be given.
Assume Hk.
Apply LRE' z Hz to the current goal.
We prove the intermediate
claim Lzz:
SNo (z + z).
An
exact proof term for the current goal is
SNo_add_SNo z z HzS HzS.
We prove the intermediate
claim Lzzpos:
0 < z + z.
We will
prove 0 + 0 < z + z.
We prove the intermediate
claim Lzzn0:
z + z ≠ 0.
Assume H5.
rewrite the current goal using H5 (from right to left) at position 2.
An exact proof term for the current goal is Lzzpos.
We prove the intermediate
claim Lzmz:
SNo (z * z).
An
exact proof term for the current goal is
SNo_mul_SNo z z HzS HzS.
Set z' to be the term
(x + z * z) :/: (z + z).
We prove the intermediate
claim Lz':
z' ∈ 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 Hzk.
An exact proof term for the current goal is Hzk.
An exact proof term for the current goal is Lzzpos.
We prove the intermediate
claim Lz'R:
z' ∈ R.
We prove the intermediate
claim Lz'S:
SNo z'.
An
exact proof term for the current goal is
real_SNo z' (LRsR z' Lz'R).
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lz'R.
We will
prove (x + z * z) :/: (z + z) < z.
We will
prove x + z * z < z * (z + z).
rewrite the current goal using
mul_SNo_distrL z z z HzS HzS HzS (from left to right).
We will
prove x + z * z < z * z + z * z.
Apply add_SNo_Lt1 x (z * z) (z * z) Hx1 Lzmz Lzmz to the current goal.
rewrite the current goal using H3 (from right to left).
rewrite the current goal using Hsx0 (from right to left).
An
exact proof term for the current goal is
mul_SNo_pos_pos z z HzS HzS Hzpos Hzpos.
An
exact proof term for the current goal is
real_SNoCut L LLsR R LRsR LLR LLne LRne LLnomax LRnomin.
∎