Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
Assume Hyln: y = eps_ l * n.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x * y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (m * n) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is int_mul_SNo m Hm n Hn.
We will prove x * y = eps_ (k + l) * (m * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x * y = (eps_ k * eps_ l) * (m * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) m n Lek Lel Lm Ln (from left to right).
We will prove x * y = (eps_ k * m) * (eps_ l * n).
Use f_equal.
An exact proof term for the current goal is Hxkm.
An exact proof term for the current goal is Hyln.
∎