Let x be given.
Assume H.
Apply H 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.
We will prove ∃k' ∈ ω, ∃m' ∈ int, - x = 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 (- m) to witness the existential quantifier.
Apply andI to the current goal.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is Hm.
We will prove - x = eps_ k * (- m).
rewrite the current goal using mul_SNo_minus_distrR (eps_ k) m (SNo_eps_ k Hk) Lm (from left to right).
We will prove - x = - eps_ k * m.
Use f_equal.
An exact proof term for the current goal is Hxkm.
∎