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