Let t be given.

Assume HtI: t ∈ unit_interval.

We will prove Rle 0 t.

We prove the intermediate claim HtR: t ∈ R.

An exact proof term for the current goal is (unit_interval_sub_R t HtI).

We prove the intermediate claim Hconj: ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t).

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) t HtI).

We prove the intermediate claim Hnlt: ¬ (Rlt t 0).

An exact proof term for the current goal is (andEL (¬ (Rlt t 0)) (¬ (Rlt 1 t)) Hconj).

An exact proof term for the current goal is (RleI 0 t real_0 HtR Hnlt).

∎