rewrite the current goal using
eps_0_1 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
An
exact proof term for the current goal is
SNoLt_tra x 0 x Hx1c SNo_0 Hx1c H2 H1.
Let N be given.
Assume HN.
We prove the intermediate
claim LN1:
SNo N.
An
exact proof term for the current goal is
nat_p_SNo N HN.
We prove the intermediate
claim LN2:
SNo (- N).
We prove the intermediate
claim LN3:
N ∈ SNoS_ ω.
An
exact proof term for the current goal is
nat_p_omega N HN.
We use
(- ordsucc N) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will
prove x < - (N + 1) + 1.
An exact proof term for the current goal is H4.
Apply L1 to the current goal.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is LN3.
An exact proof term for the current goal is IHN H4 H3.
Apply L1 to the current goal.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is LN3.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is LN3.
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 N be given.
Assume HN.
Apply HN to the current goal.
Let N' be given.
Assume HN'.
Apply HN' to the current goal.
Apply L1a N' (omega_nat_p N' HN'1) HN'2 to the current goal.
Apply L1a N' (omega_nat_p N' HN'1) HN'2 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is HN2.
We will
prove - N < - N'.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is HN'2.
An exact proof term for the current goal is HN2.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq1.
Apply andI to the current goal.
An exact proof term for the current goal is Hq2.
An exact proof term for the current goal is H1.
Apply L1 to the current goal.
rewrite the current goal using H1 (from left to right).
We use
(q + eps_ (ordsucc k)) to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hq3.