Apply Hf2 n Hn to the current goal.
Assume H.
Apply H to the current goal.
Apply and3I to the current goal.
We will
prove - (f n + eps_ n) < x.
An exact proof term for the current goal is Hf2b.
An exact proof term for the current goal is Hf2a.
Let i be given.
Assume Hi.
We prove the intermediate
claim Li:
i ∈ ω.
rewrite the current goal using
beta ω (λn ⇒ - f n) i Li (from left to right).
We will
prove - f n < - f i.
An exact proof term for the current goal is Hf2c i Hi.