Let q be given.
Assume Hq: q ∈ SNoS_ ω.
Apply SNoS_omega_diadic_rational_p q Hq 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 Hqkm: q = eps_ k * m.
We prove the intermediate claim LkN: nat_p k.
An exact proof term for the current goal is omega_nat_p k Hk.
We will prove q ∈ {x ∈ real|∃m ∈ int, ∃n ∈ ω ∖ {0}, x = m :/: n}.
Apply SepI to the current goal.
We will prove q ∈ real.
Apply SNoS_omega_real to the current goal.
An exact proof term for the current goal is Hq.
We will prove ∃m ∈ int, ∃n ∈ ω ∖ {0}, q = m :/: n.
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 ∃n ∈ ω ∖ {0}, q = m :/: n.
We prove the intermediate claim L2kN: nat_p (2 ^ k).
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 k LkN.
We prove the intermediate claim L2kS: SNo (2 ^ k).
An exact proof term for the current goal is nat_p_SNo (2 ^ k) L2kN.
We prove the intermediate claim L2knz: 2 ^ k ≠ 0.
Assume H1: 2 ^ k = 0.
Apply neq_1_0 to the current goal.
We will prove 1 = 0.
rewrite the current goal using mul_SNo_eps_power_2 k LkN (from right to left).
We will prove eps_ k * 2 ^ k = 0.
rewrite the current goal using H1 (from left to right).
We will prove eps_ k * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR (eps_ k) (SNo_eps_ k Hk).
We use 2 ^ k to witness the existential quantifier.
Apply andI to the current goal.
We will prove 2 ^ k ∈ ω ∖ {0}.
Apply setminusI to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is L2kN.
Assume H1: 2 ^ k ∈ {0}.
Apply L2knz to the current goal.
We will prove 2 ^ k = 0.
An exact proof term for the current goal is SingE 0 (2 ^ k) H1.
We will prove q = m :/: (2 ^ k).
We will prove q = m * recip_SNo (2 ^ k).
rewrite the current goal using Hqkm (from left to right).
We will prove eps_ k * m = m * recip_SNo (2 ^ k).
rewrite the current goal using recip_SNo_pow_2 k LkN (from left to right).
An exact proof term for the current goal is mul_SNo_com (eps_ k) m (SNo_eps_ k Hk) (int_SNo m Hm).
∎