We will prove eps_ 1 ∈ R.

We prove the intermediate claim H1omega: 1 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 1 nat_1).

We prove the intermediate claim Heps1SNoS: eps_ 1 ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).

An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).

∎