We will prove Rlt (eps_ 1) 1.
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 H0Ord: ordinal 0.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).
We prove the intermediate claim HepsLtE0: eps_ 1 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).
We prove the intermediate claim HepsLt1S: (eps_ 1) < 1.
rewrite the current goal using (eps_0_1) (from right to left) at position 2.
An exact proof term for the current goal is HepsLtE0.
An exact proof term for the current goal is (RltI (eps_ 1) 1 eps_1_in_R real_1 HepsLt1S).
∎