Let a and b be given.

Assume Hab: Rle a b.

We will prove a ∈ closed_interval a b.

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (RleE_left a b Hab).

We prove the intermediate claim Hnlt_ba: ¬ (Rlt b a).

An exact proof term for the current goal is (RleE_nlt a b Hab).

We prove the intermediate claim HCI_def: closed_interval a b = {t ∈ R|¬ (Rlt t a) ∧ ¬ (Rlt b t)}.

Use reflexivity.

rewrite the current goal using HCI_def (from left to right).

Apply (SepI R (λt : set ⇒ ¬ (Rlt t a) ∧ ¬ (Rlt b t)) a HaR) to the current goal.

Apply andI to the current goal.

Assume Hlt: Rlt a a.

We will prove False.

We prove the intermediate claim Halt: a < a.

An exact proof term for the current goal is (RltE_lt a a Hlt).

An exact proof term for the current goal is ((SNoLt_irref a) Halt).

An exact proof term for the current goal is Hnlt_ba.

∎