Let a, b and x be given.
Assume HaR HbR HxR HxInab.
We prove the intermediate claim HxabProp: Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z ∧ Rlt z b) x HxInab).
We prove the intermediate claim Hax: Rlt a x.
An exact proof term for the current goal is (andEL (Rlt a x) (Rlt x b) HxabProp).
We prove the intermediate claim Hxb: Rlt x b.
An exact proof term for the current goal is (andER (Rlt a x) (Rlt x b) HxabProp).
Apply (rational_dense_between_reals a x HaR HxR Hax) to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume Hq1Prop: Rlt a q1 ∧ Rlt q1 x.
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
We prove the intermediate claim Haq1: Rlt a q1.
An exact proof term for the current goal is (andEL (Rlt a q1) (Rlt q1 x) Hq1Prop).
We prove the intermediate claim Hq1x: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt a q1) (Rlt q1 x) Hq1Prop).
Apply (rational_dense_between_reals x b HxR HbR Hxb) to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hq2Prop: Rlt x q2 ∧ Rlt q2 b.
We prove the intermediate claim Hq2R: q2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).
We prove the intermediate claim Hxq2: Rlt x q2.
An exact proof term for the current goal is (andEL (Rlt x q2) (Rlt q2 b) Hq2Prop).
We prove the intermediate claim Hq2b: Rlt q2 b.
An exact proof term for the current goal is (andER (Rlt x q2) (Rlt q2 b) Hq2Prop).
We use q1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq1Q.
We use q2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq2Q.
Apply andI to the current goal.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) x HxR (andI (Rlt q1 x) (Rlt x q2) Hq1x Hxq2)).
Let y be given.
Assume Hy: y ∈ open_interval q1 q2.
We will prove y ∈ open_interval a b.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y Hy).
We prove the intermediate claim HyProp: Rlt q1 y ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y Hy).
We prove the intermediate claim Hq1y: Rlt q1 y.
An exact proof term for the current goal is (andEL (Rlt q1 y) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (Rlt q1 y) (Rlt y q2) HyProp).
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 Hq1S: SNo q1.
An exact proof term for the current goal is (real_SNo q1 Hq1R).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Hq2S: SNo q2.
An exact proof term for the current goal is (real_SNo q2 Hq2R).
We prove the intermediate claim Haq1lt: a < q1.
An exact proof term for the current goal is (RltE_lt a q1 Haq1).
We prove the intermediate claim Hq1ylt: q1 < y.
An exact proof term for the current goal is (RltE_lt q1 y Hq1y).
We prove the intermediate claim Hyq2lt: y < q2.
An exact proof term for the current goal is (RltE_lt y q2 Hyq2).
We prove the intermediate claim Hq2blt: q2 < b.
An exact proof term for the current goal is (RltE_lt q2 b Hq2b).
We prove the intermediate claim Haylt: a < y.
An exact proof term for the current goal is (SNoLt_tra a q1 y HaS Hq1S HyS Haq1lt Hq1ylt).
We prove the intermediate claim Hyblt: y < b.
An exact proof term for the current goal is (SNoLt_tra y q2 b HyS Hq2S HbS Hyq2lt Hq2blt).
We prove the intermediate claim Hay: Rlt a y.
An exact proof term for the current goal is (RltI a y HaR HyR Haylt).
We prove the intermediate claim Hyb: Rlt y b.
An exact proof term for the current goal is (RltI y b HyR HbR Hyblt).
We prove the intermediate claim Hconj: Rlt a y ∧ Rlt y b.
Apply andI to the current goal.
An exact proof term for the current goal is Hay.
An exact proof term for the current goal is Hyb.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a z ∧ Rlt z b) y HyR Hconj).
∎