We will prove 1 ∈ unit_interval_right_half.
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is one_in_unit_interval.
We prove the intermediate claim Hnlt: ¬ (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 unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) 1 H1I Hnlt).
∎