Apply Lf'0b to the current goal.
Assume H H6.
Apply H to the current goal.
Assume H4 H5.
Apply and4I to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Let i be given.
Assume Hi.
An
exact proof term for the current goal is
EmptyE i Hi.
Let n be given.
Assume Hn.
Apply IHn to the current goal.
Assume IHn123 IHn4.
Apply IHn123 to the current goal.
Assume IHn12 IHn3.
Apply IHn12 to the current goal.
Assume IHn1 IHn2.
Assume _ _.
Assume _.
Let q be given.
Assume Hq.
Apply Hq to the current goal.
Assume Hq1 Hq.
Apply Hq to the current goal.
Assume Hq2 Hq3.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply SNoLtLe_or (f' n) q IHn1c Hq1c to the current goal.
We use q to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hq1.
An exact proof term for the current goal is Hq2.
An exact proof term for the current goal is Hq3.
An exact proof term for the current goal is H4.
We prove the intermediate
claim L1ba:
SNo (- f' n).
An
exact proof term for the current goal is
SNo_minus_SNo (f' n) IHn1c.
We prove the intermediate
claim L1bb:
SNo (x + - f' n).
An
exact proof term for the current goal is
SNo_add_SNo x (- f' n) H1 L1ba.
Assume H5.
Apply H5 to the current goal.
Let k be given.
Assume H5.
Apply H5 to the current goal.
We use
(f' n + eps_ (ordsucc k)) to
witness the existential quantifier.
We prove the intermediate
claim Lk1:
ordsucc k ∈ ω.
Assume _ _.
Assume _.
Apply and4I to the current goal.
An exact proof term for the current goal is Lk3.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Lk1.
We will
prove f' n + eps_ k ≤ x.
We will
prove f' n + eps_ k ≤ f' n + (- f' n + x).
rewrite the current goal using
add_SNo_com (- f' n) x L1ba H1 (from left to right).
We will
prove f' n + eps_ k ≤ f' n + (x + - f' n).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hq3.
We prove the intermediate
claim L1bd:
0 < x + - f' n.
We will
prove 0 + f' n < (x + - f' n) + f' n.
rewrite the current goal using
add_SNo_0L (f' n) IHn1c (from left to right).
rewrite the current goal using
add_SNo_minus_R2' x (f' n) H1 IHn1c (from left to right).
An exact proof term for the current goal is IHn2.
We prove the intermediate
claim L1be:
f' n = x.
Apply H2 (f' n) IHn1 to the current goal.
Let k be given.
Assume Hk.
rewrite the current goal using
abs_SNo_dist_swap (f' n) x IHn1c H1 (from left to right).
rewrite the current goal using
pos_abs_SNo (x + - f' n) L1bd (from left to right).
An exact proof term for the current goal is H6.
Apply H5 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
An exact proof term for the current goal is H6.
rewrite the current goal using L1be (from right to left) at position 1.
An exact proof term for the current goal is IHn2.
rewrite the current goal using Lf'S n Hn (from left to right).
Apply L1c to the current goal.
Assume H H7.
Apply H to the current goal.
Assume H H6.
Apply H to the current goal.
Assume H4 H5.
Apply and4I to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Let i be given.
Apply ordsuccE n i Hi to the current goal.
An exact proof term for the current goal is Hfi.
An exact proof term for the current goal is IHn1c.
Assume _ _ H9 _.
An exact proof term for the current goal is H9.
Apply IHn to the current goal.
Assume _.
An exact proof term for the current goal is IHn4 i H8 Hfi.
An exact proof term for the current goal is H7.
rewrite the current goal using H8 (from left to right).
rewrite the current goal using
beta ω f' n (nat_p_omega n Hn) (from left to right).
An exact proof term for the current goal is H7.