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

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.

rewrite the current goal using Hxkm (from left to right).

We will prove eps_ k * m ∈ SNoS_ ω.

We prove the intermediate claim L1: ∀n ∈ ω, eps_ k * n ∈ SNoS_ ω.

Let n be given.

Assume Hn: n ∈ ω.

We will prove eps_ k * n ∈ SNoS_ ω.

An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).

We prove the intermediate claim L2: ∀n ∈ ω, eps_ k * (- n) ∈ SNoS_ ω.

Let n be given.

Assume Hn: n ∈ ω.

We will prove eps_ k * (- n) ∈ SNoS_ ω.

rewrite the current goal using mul_SNo_minus_distrR (eps_ k) n (SNo_eps_ k Hk) (omega_SNo n Hn) (from left to right).

Apply minus_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is nonneg_diadic_rational_p_SNoS_omega k Hk n (omega_nat_p n Hn).

An exact proof term for the current goal is int_SNo_cases (λm ⇒ eps_ k * m ∈ SNoS_ ω) L1 L2 m Hm.

∎