Assume H.
Apply H to the current goal.
Let m'' be given.
Assume H.
Apply H to the current goal.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
Apply and3I to the current goal.
We prove the intermediate
claim L1aa:
m ∈ 2.
An exact proof term for the current goal is H5.
Apply cases_2 m L1aa (λi ⇒ m ≠ i) to the current goal.
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using Hm'm'' (from left to right).
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is Hxm1.
Apply nat_inv m'' Hm'' to the current goal.
Apply Hxn2 to the current goal.
rewrite the current goal using H4 (from right to left).
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using Hm'm'' (from left to right).
rewrite the current goal using Hm''0 (from left to right).
Use reflexivity.
Assume H.
Apply H to the current goal.
Let m''' be given.
Assume H.
Apply H to the current goal.
We use m' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm'.
Apply and3I to the current goal.
rewrite the current goal using Hm'm'' (from left to right).
We will
prove 2 ≤ 1 + m''.
rewrite the current goal using Hm''m''' (from left to right).
We will
prove 2 ≤ 1 + 1 + m'''.
We will
prove 2 ≤ (1 + 1) + m'''.
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
We will
prove 2 ≤ 2 + m'''.
rewrite the current goal using
add_SNo_0R 2 SNo_2 (from right to left) at position 1.
We will
prove 2 + 0 ≤ 2 + m'''.
rewrite the current goal using H4 (from right to left).
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using H4 (from right to left).
rewrite the current goal using Hmm' (from left to right).
Apply L1a to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim Lk:
nat_p k.
An
exact proof term for the current goal is
omega_nat_p k Hk.
We prove the intermediate
claim LkS:
SNo k.
An
exact proof term for the current goal is
nat_p_SNo k Lk.
We use k to witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
We will
prove k ∈ SNoL x.
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Hx1.
An exact proof term for the current goal is LkS.
An exact proof term for the current goal is H4.
Apply SNoLtLe_tra k x k LkS Hx1 LkS Hkx to the current goal.
rewrite the current goal using H4 (from right to left).
Apply SNoLt_tra k x k LkS Hx1 LkS Hkx to the current goal.
An exact proof term for the current goal is Hkx.
An exact proof term for the current goal is H2k.
rewrite the current goal using
add_SNo_1_1_2 (from right to left).
rewrite the current goal using
mul_SNo_oneL k LkS (from left to right).
We will
prove 1 + k < k + k.
An exact proof term for the current goal is H2k.