We will prove Rlt 0 (eps_ 1).

We prove the intermediate claim H1omega: 1 ∈ ω.

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

An exact proof term for the current goal is (RltI 0 (eps_ 1) real_0 eps_1_in_R (SNo_eps_pos 1 H1omega)).

∎