We will prove eps_ 1 ∈ unit_interval.
We prove the intermediate claim Hnlt_eps10: ¬ (Rlt (eps_ 1) 0).
An exact proof term for the current goal is (not_Rlt_sym 0 (eps_ 1) eps_1_pos_R).
We prove the intermediate claim Hnlt_1eps1: ¬ (Rlt 1 (eps_ 1)).
An exact proof term for the current goal is (not_Rlt_sym (eps_ 1) 1 eps_1_lt1_R).
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (eps_ 1) eps_1_in_R (andI (¬ (Rlt (eps_ 1) 0)) (¬ (Rlt 1 (eps_ 1))) Hnlt_eps10 Hnlt_1eps1)).
∎