Let a and b be given.

Assume Hab: Rle a b.

We will prove b ∈ closed_interval a b.

We prove the intermediate claim HbR: b ∈ R.

An exact proof term for the current goal is (RleE_right 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)) b HbR) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hnlt_ba.

Assume Hlt: Rlt b b.

We will prove False.

We prove the intermediate claim Halt: b < b.

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

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

∎