Let t be given.

Assume HtI: t ∈ unit_interval.

We will prove Rle t 1.

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 1 t).

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

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

∎