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.
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.
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.
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.
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.
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.