Let m be given.
We prove the intermediate
claim Lmo:
ordinal m.
We prove the intermediate
claim LmS:
SNo m.
An
exact proof term for the current goal is
ordinal_SNo m Lmo.
We prove the intermediate
claim L1:
∀k ∈ ω, - n + m = k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
An exact proof term for the current goal is Hk.
We prove the intermediate
claim L2:
∀k ∈ ω, - n + m = - k → 1 + (- n + m) ∈ int.
Let k be given.
Assume Hk He.
rewrite the current goal using He (from left to right).
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
Assume H1.
Apply H1 to the current goal.
Let k' be given.
Assume H1.
Apply H1 to the current goal.
rewrite the current goal using H2 (from left to right).
We will
prove - k' ∈ int.
An
exact proof term for the current goal is
nat_p_omega k' H1.
Use reflexivity.
∎