We will
prove ∀w ∈ L, ∃w' ∈ L, w < w'.
Let w be given.
Assume Hw.
Let k be given.
Apply L1L w Hw to the current goal.
We prove the intermediate
claim Lwmw:
SNo (w * w).
An
exact proof term for the current goal is
SNo_mul_SNo w w Hw1 Hw1.
We prove the intermediate
claim Lwpw:
SNo (w + w).
An
exact proof term for the current goal is
SNo_add_SNo w w Hw1 Hw1.
We prove the intermediate
claim L1a:
∃z, z ∈ R_ (ordsucc k).
We use
1 to
witness the existential quantifier.
Assume _.
Apply H5 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 SepI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H4.
rewrite the current goal using H4 (from right to left) at position 2.
An exact proof term for the current goal is H2.
We prove the intermediate
claim L1a1:
1 ∈ L_ k.
Assume _.
Apply H5 to the current goal.
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).
Apply ReplI to the current goal.
Apply SepI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H4.
An
exact proof term for the current goal is
SNoLt_0_1.
We prove the intermediate
claim L1a2:
0 < 1 + 1.
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
An
exact proof term for the current goal is
SNoLt_0_2.
We use z to witness the existential quantifier.
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 1 L1a1 1 L1a1 L1a2.
Apply L1a to the current goal.
Let z be given.
We prove the intermediate
claim Lz:
z ∈ R.
Apply L1R z Lz to the current goal.
We prove the intermediate
claim Lwmz:
SNo (w * z).
An
exact proof term for the current goal is
SNo_mul_SNo w z Hw1 Hz1.
We prove the intermediate
claim Lwpz:
SNo (w + z).
An
exact proof term for the current goal is
SNo_add_SNo w z Hw1 Hz1.
We prove the intermediate
claim Lzpos:
0 < z.
An exact proof term for the current goal is H4.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hz3.
We prove the intermediate
claim Lwpzpos:
0 < w + z.
rewrite the current goal using
add_SNo_0L z Hz1 (from right to left) at position 1.
We will
prove 0 + z ≤ w + z.
We prove the intermediate
claim Lwpzn0:
w + z ≠ 0.
rewrite the current goal using H4 (from right to left) at position 2.
An exact proof term for the current goal is Lwpzpos.
Set w' to be the term
(x + w * z) :/: (w + z).
rewrite the current goal using
tuple_2_0_eq (from left to right).
We prove the intermediate
claim LwLk:
w ∈ L_ (ordsucc k).
Assume _.
Apply H5 to the current goal.
An exact proof term for the current goal is H3.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using
div_mul_SNo_invL w (w + z) Hw1 Lwpz Lwpzn0 (from right to left) at position 1.
We will
prove (w * (w + z)) :/: (w + z) < w'.
We will
prove w * (w + z) < x + w * z.
rewrite the current goal using
mul_SNo_distrL w w z Hw1 Hw1 Hz1 (from left to right).
We will
prove w * w + w * z < x + w * z.
Apply add_SNo_Lt1 (w * w) (w * z) x Lwmw Lwmz Hx to the current goal.
An exact proof term for the current goal is Hw3.