We will prove 0 ∈ unit_interval_left_half.

We prove the intermediate claim H0I: 0 ∈ unit_interval.

An exact proof term for the current goal is zero_in_unit_interval.

An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) 0 H0I (not_Rlt_sym 0 (eps_ 1) eps_1_pos_R)).

∎