Let x be given.

Assume Hx: x ∈ R ∖ halfopen_interval_left a b.

We will prove x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|¬ (Rlt x0 b)}.

We prove the intermediate claim Hpair: x ∈ R ∧ x ∉ halfopen_interval_left a b.

An exact proof term for the current goal is (setminusE R (halfopen_interval_left a b) x Hx).

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (andEL (x ∈ R) (x ∉ halfopen_interval_left a b) Hpair).

We prove the intermediate claim HxNotI: x ∉ halfopen_interval_left a b.

An exact proof term for the current goal is (andER (x ∈ R) (x ∉ halfopen_interval_left a b) Hpair).

Apply (xm (Rlt x a)) to the current goal.

Assume Hxa: Rlt x a.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 a) x HxR Hxa).

Assume Hnxa: ¬ (Rlt x a).

Apply (xm (Rlt x b)) to the current goal.

Assume Hxb: Rlt x b.

We prove the intermediate claim HxinI: x ∈ halfopen_interval_left a b.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) x HxR (andI (¬ (Rlt x a)) (Rlt x b) Hnxa Hxb)).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HxNotI HxinI).

Assume Hnxb: ¬ (Rlt x b).

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 b)) x HxR Hnxb).

Let x be given.

Assume Hx: x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|¬ (Rlt x0 b)}.

We will prove x ∈ R ∖ halfopen_interval_left a b.

Apply (binunionE {x0 ∈ R|Rlt x0 a} {x0 ∈ R|¬ (Rlt x0 b)} x Hx) to the current goal.

Assume HxL: x ∈ {x0 ∈ R|Rlt x0 a}.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt x0 a) x HxL).

We prove the intermediate claim Hxa: Rlt x a.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 a) x HxL).

We will prove x ∈ R ∖ halfopen_interval_left a b.

Apply (setminusI R (halfopen_interval_left a b) x HxR) to the current goal.

Assume HxinI: x ∈ halfopen_interval_left a b.

We prove the intermediate claim Hprop: ¬ (Rlt x a) ∧ Rlt x b.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) x HxinI).

We prove the intermediate claim Hnxa: ¬ (Rlt x a).

An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (Rlt x b) Hprop).

An exact proof term for the current goal is (Hnxa Hxa).

Assume HxRr: x ∈ {x0 ∈ R|¬ (Rlt x0 b)}.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 b)) x HxRr).

We prove the intermediate claim Hnxb: ¬ (Rlt x b).

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 b)) x HxRr).

We will prove x ∈ R ∖ halfopen_interval_left a b.

Apply (setminusI R (halfopen_interval_left a b) x HxR) to the current goal.

Assume HxinI: x ∈ halfopen_interval_left a b.

We prove the intermediate claim Hprop: ¬ (Rlt x a) ∧ Rlt x b.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) x HxinI).

We prove the intermediate claim Hxb: Rlt x b.

An exact proof term for the current goal is (andER (¬ (Rlt x a)) (Rlt x b) Hprop).

An exact proof term for the current goal is (Hnxb Hxb).