Let n be given.

Assume Hn: n ∈ ω.

Apply int_SNo_cases to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Apply Subq_omega_int to the current goal.

We will prove n + m ∈ ω.

An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.

Let m be given.

Assume Hm: m ∈ ω.

We will prove n + - m ∈ int.

rewrite the current goal using add_SNo_com n (- m) (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (SNo_minus_SNo m (ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)))) (from left to right).

We will prove - m + n ∈ int.

An exact proof term for the current goal is int_add_SNo_lem m Hm n (omega_nat_p n Hn).

Let n be given.

Assume Hn: n ∈ ω.

Apply int_SNo_cases to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

We will prove - n + m ∈ int.

An exact proof term for the current goal is int_add_SNo_lem n Hn m (omega_nat_p m Hm).

Let m be given.

Assume Hm: m ∈ ω.

We will prove - n + - m ∈ int.

We prove the intermediate claim Ln: SNo n.

An exact proof term for the current goal is ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn)).

We prove the intermediate claim Lm: SNo m.

An exact proof term for the current goal is ordinal_SNo m (nat_p_ordinal m (omega_nat_p m Hm)).

rewrite the current goal using minus_add_SNo_distr n m Ln Lm (from right to left).

Apply int_minus_SNo_omega to the current goal.

We will prove n + m ∈ ω.

An exact proof term for the current goal is add_SNo_In_omega n Hn m Hm.