Let a, x and b be given.
Assume HaR: a ∈ R.
Assume HxR: x ∈ R.
Assume HbR: b ∈ R.
Assume Hax: Rle a x.
Let y be given.
Assume Hy: y ∈ halfopen_interval_left x b.
We will prove y ∈ halfopen_interval_left a b.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t b) y Hy).
We prove the intermediate claim Hyprop: ¬ (Rlt y x) ∧ Rlt y b.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t b) y Hy).
We prove the intermediate claim Hynltx: ¬ (Rlt y x).
An exact proof term for the current goal is (andEL (¬ (Rlt y x)) (Rlt y b) Hyprop).
We prove the intermediate claim Hyltb: Rlt y b.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y b) Hyprop).
We prove the intermediate claim Hynlta: ¬ (Rlt y a).
Assume Hlt: Rlt y a.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hnltxa: ¬ (Rlt x a).
An exact proof term for the current goal is (RleE_nlt a x Hax).
We prove the intermediate claim Hyltx: Rlt y x.
Apply (SNoLt_trichotomy_or_impred x a HxS HaS (Rlt y x)) to the current goal.
Assume Hxa: x < a.
We prove the intermediate claim Hxlt: Rlt x a.
An exact proof term for the current goal is (RltI x a HxR HaR Hxa).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnltxa Hxlt).
Assume Hxeq: x = a.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is Hlt.
Assume Haxlt: a < x.
We prove the intermediate claim Hylt_a: y < a.
An exact proof term for the current goal is (RltE_lt y a Hlt).
We prove the intermediate claim Hylt_x: y < x.
An exact proof term for the current goal is (SNoLt_tra y a x HyS HaS HxS Hylt_a Haxlt).
An exact proof term for the current goal is (RltI y x HyR HxR Hylt_x).
An exact proof term for the current goal is (Hynltx Hyltx).
We prove the intermediate claim Hyprop2: ¬ (Rlt y a) ∧ Rlt y b.
Apply andI to the current goal.
An exact proof term for the current goal is Hynlta.
An exact proof term for the current goal is Hyltb.
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t a) ∧ Rlt t b) y HyR Hyprop2).
∎