Let n be given.

Assume Hn: n ∈ ω.

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 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 mul_SNo_In_omega n Hn m Hm.

Let m be given.

Assume Hm: m ∈ ω.

We prove the intermediate claim Lmn: nat_p m.

An exact proof term for the current goal is omega_nat_p m Hm.

We prove the intermediate claim Lmo: ordinal m.

An exact proof term for the current goal is nat_p_ordinal m Lmn.

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 * (- m) ∈ int.

rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).

We will prove (- m) * n ∈ int.

rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).

We will prove - (m * n) ∈ int.

Apply int_minus_SNo to the current goal.

We will prove m * n ∈ int.

Apply Subq_omega_int to the current goal.

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

Let n be given.

Assume Hn: n ∈ ω.

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 int_SNo_cases to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

We prove the intermediate claim Lmn: nat_p m.

An exact proof term for the current goal is omega_nat_p m Hm.

We prove the intermediate claim Lmo: ordinal m.

An exact proof term for the current goal is nat_p_ordinal m Lmn.

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) * m ∈ int.

rewrite the current goal using mul_SNo_minus_distrL n m LnS LmS (from left to right).

We will prove - (n * m) ∈ int.

Apply int_minus_SNo to the current goal.

We will prove n * m ∈ int.

Apply Subq_omega_int to the current goal.

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

Let m be given.

Assume Hm: m ∈ ω.

We prove the intermediate claim Lmn: nat_p m.

An exact proof term for the current goal is omega_nat_p m Hm.

We prove the intermediate claim Lmo: ordinal m.

An exact proof term for the current goal is nat_p_ordinal m Lmn.

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) * (- m) ∈ int.

rewrite the current goal using mul_SNo_minus_distrL n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).

We will prove - (n * (- m)) ∈ int.

rewrite the current goal using mul_SNo_com n (- m) LnS (SNo_minus_SNo m LmS) (from left to right).

We will prove - ((- m) * n) ∈ int.

rewrite the current goal using mul_SNo_minus_distrL m n LmS LnS (from left to right).

We will prove - - (m * n) ∈ int.

rewrite the current goal using minus_SNo_invol (m * n) (SNo_mul_SNo m n LmS LnS) (from left to right).

We will prove m * n ∈ int.

Apply Subq_omega_int to the current goal.

We will prove m * n ∈ ω.

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