We will prove 0 ∈ unit_interval.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hnlt00: ¬ (Rlt 0 0).
An exact proof term for the current goal is (not_Rlt_refl 0 H0R).
We prove the intermediate claim H0lt1: Rlt 0 1.
An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).
We prove the intermediate claim Hnlt10: ¬ (Rlt 1 0).
An exact proof term for the current goal is (not_Rlt_sym 0 1 H0lt1).
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) 0 H0R (andI (¬ (Rlt 0 0)) (¬ (Rlt 1 0)) Hnlt00 Hnlt10)).
∎