Let m be given.
Assume Hm.
We will prove ∃k ∈ ω, ∃m' ∈ int, m = eps_ k * m'.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is nat_p_omega 0 nat_0.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We will prove m = eps_ 0 * m.
rewrite the current goal using eps_0_1 (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneL m (int_SNo m Hm).
∎