Let k be given.
Assume Hk.
We will prove ∃k' ∈ ω, ∃m ∈ int, eps_ k = eps_ k' * m.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
We will prove eps_ k = eps_ k * 1.
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneR (eps_ k) (SNo_eps_ k Hk).
∎