We will prove 1 ∈ unit_interval.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
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).
We prove the intermediate claim Hnlt11: ¬ (Rlt 1 1).
An exact proof term for the current goal is (not_Rlt_refl 1 H1R).
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) 1 H1R (andI (¬ (Rlt 1 0)) (¬ (Rlt 1 1)) Hnlt10 Hnlt11)).
∎