We will prove eps_ 1 ∈ unit_interval_right_half.
We prove the intermediate claim HeI: eps_ 1 ∈ unit_interval.
An exact proof term for the current goal is eps_1_in_unit_interval.
We prove the intermediate claim Hnlt: ¬ (Rlt (eps_ 1) (eps_ 1)).
An exact proof term for the current goal is (not_Rlt_refl (eps_ 1) eps_1_in_R).
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) (eps_ 1) HeI Hnlt).
∎