Let x be given.
Assume Hx1 Hx2 Hx3.
Assume Hx1a Hx1b Hx1c Hx1d.
Let N be given.
Assume HN.
Apply HN to the current goal.
We prove the intermediate
claim LN:
SNo N.
An
exact proof term for the current goal is
omega_SNo N HN1.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1.
An exact proof term for the current goal is HN2.
An exact proof term for the current goal is H1.
We prove the intermediate
claim L2N:
SNo (2 ^ N).
We prove the intermediate
claim L1:
2 ^ N ≤ 2 ^ N * eps_ N * N.
rewrite the current goal using
mul_SNo_oneR (2 ^ N) L2N (from right to left) at position 1.
An
exact proof term for the current goal is
SNo_1.
An exact proof term for the current goal is H1.
We will
prove 2 ^ N < 2 ^ N.
rewrite the current goal using
mul_SNo_oneL N LN (from right to left) at position 2.
We will
prove 2 ^ N ≤ 1 * N.
An exact proof term for the current goal is L1.
∎