Let m and n be given.
Assume Hn.
We prove the intermediate claim Ln: SNo n.
Apply omega_SNo to the current goal.
An exact proof term for the current goal is Hn.
Apply nat_ind to the current goal.
We will prove m ∈ n + 0 → m ∈ n ∨ m + - n ∈ 0.
rewrite the current goal using add_SNo_0R n Ln (from left to right).
Assume H1.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Let k be given.
Assume Hk.
Assume IHk: m ∈ n + k → m ∈ n ∨ m + - n ∈ k.
rewrite the current goal using add_SNo_1_ordsucc k (nat_p_omega k Hk) (from right to left) at position 1.
rewrite the current goal using add_SNo_assoc n k 1 Ln (nat_p_SNo k Hk) SNo_1 (from left to right).
rewrite the current goal using add_SNo_1_ordsucc (n + k) (add_SNo_In_omega n Hn k (nat_p_omega k Hk)) (from left to right).
Assume H1: m ∈ ordsucc (n + k).
Apply ordsuccE (n + k) m H1 to the current goal.
Assume H2: m ∈ n + k.
Apply IHk H2 to the current goal.
Assume H3: m ∈ n.
Apply orIL to the current goal.
An exact proof term for the current goal is H3.
Assume H3: m + - n ∈ k.
Apply orIR to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H3.
Assume H2: m = n + k.
Apply orIR to the current goal.
rewrite the current goal using H2 (from left to right).
We will prove (n + k) + - n ∈ ordsucc k.
rewrite the current goal using add_SNo_com (n + k) (- n) (SNo_add_SNo n k Ln (nat_p_SNo k Hk)) (SNo_minus_SNo n Ln) (from left to right).
rewrite the current goal using add_SNo_minus_L2 n k Ln (nat_p_SNo k Hk) (from left to right).
Apply ordsuccI2 to the current goal.
∎