Let x be given.
Assume HxR Hxnn.
Apply real_E x HxR to the current goal.
Let m be given.
Assume Hm.
Apply IHm to the current goal.
An exact proof term for the current goal is H3.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_p_omega m Hm.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H2.
Let q be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
rewrite the current goal using
eps_0_1 (from left to right).
Let m be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim Lq:
SNo q.
Apply L1 (ordsucc m) to the current goal.
An exact proof term for the current goal is Hm.
We prove the intermediate
claim Lq1:
SNo (q + 1).
An exact proof term for the current goal is Lq.
An
exact proof term for the current goal is
SNo_1.
We will
prove SNo (q + 1).
An exact proof term for the current goal is Lq1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is Lq.
An
exact proof term for the current goal is
SNo_1.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H2.
rewrite the current goal using L3 (from left to right).
∎