Let n be given.
Assume Hn.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Lnn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is ordinal_SNo n Lno.
Apply nat_ind to the current goal.
We will prove - n + 0 ∈ int.
rewrite the current goal using add_SNo_0R (- n) (SNo_minus_SNo n LnS) (from left to right).
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: - n + m ∈ int.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Hm.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is ordinal_SNo m Lmo.
We will prove - n + ordsucc m ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq m Lmo (from left to right).
We will prove - n + (1 + m) ∈ int.
rewrite the current goal using add_SNo_com_3_0_1 (- n) 1 m (SNo_minus_SNo n LnS) SNo_1 LmS (from left to right).
We will prove 1 + (- n + m) ∈ int.
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).
We will prove 1 + k ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k (nat_p_ordinal k (omega_nat_p k Hk)) (from right to left).
We will prove ordsucc k ∈ int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
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).
We will prove 1 + - k ∈ int.
Apply nat_inv k (omega_nat_p k Hk) to the current goal.
Assume H1: k = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0R 1 SNo_1 (from left to right).
We will prove 1 ∈ int.
Apply Subq_omega_int to the current goal.
We will prove 1 ∈ ω.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
Assume H1.
Apply H1 to the current goal.
Let k' be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: nat_p k'.
Assume H2: k = ordsucc k'.
rewrite the current goal using H2 (from left to right).
We will prove 1 + - (ordsucc k') ∈ int.
rewrite the current goal using ordinal_ordsucc_SNo_eq k' (nat_p_ordinal k' H1) (from left to right).
We will prove 1 + - (1 + k') ∈ int.
rewrite the current goal using minus_add_SNo_distr 1 k' SNo_1 (ordinal_SNo k' (nat_p_ordinal k' H1)) (from left to right).
We will prove 1 + - 1 + - k' ∈ int.
rewrite the current goal using add_SNo_minus_L2' 1 (- k') SNo_1 (SNo_minus_SNo k' (ordinal_SNo k' (nat_p_ordinal k' H1))) (from left to right).
We will prove - k' ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is nat_p_omega k' H1.
Apply int_SNo_cases (λx ⇒ - n + m = x → 1 + (- n + m) ∈ int) L1 L2 (- n + m) IHm to the current goal.
Use reflexivity.
∎