Let x be given.

Assume HxU.

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 HxU).

We prove the intermediate claim Hxb: Rlt x b.

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

We prove the intermediate claim H0omega: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

Set e0 to be the term eps_ 0.

We prove the intermediate claim He0SNoS: e0 ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega 0 H0omega).

We prove the intermediate claim He0R: e0 ∈ R.

An exact proof term for the current goal is (SNoS_omega_real e0 He0SNoS).

We prove the intermediate claim He0S: SNo e0.

An exact proof term for the current goal is (real_SNo e0 He0R).

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 HmE0R: minus_SNo e0 ∈ R.

An exact proof term for the current goal is (real_minus_SNo e0 He0R).

We prove the intermediate claim HmE0S: SNo (minus_SNo e0).

An exact proof term for the current goal is (real_SNo (minus_SNo e0) HmE0R).

We prove the intermediate claim HaR: add_SNo x (minus_SNo e0) ∈ R.

An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo e0) HmE0R).

Set a0 to be the term add_SNo x (minus_SNo e0).

Set I to be the term open_interval a0 b.

We prove the intermediate claim HIStd: I ∈ R_standard_basis.

We prove the intermediate claim HIa: I ∈ {open_interval a0 bb|bb ∈ R}.

An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a0 bb) b HbR).

An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a0 I HaR HIa).

We prove the intermediate claim HxInI: x ∈ I.

We prove the intermediate claim Hxlt: x < add_SNo x e0.

An exact proof term for the current goal is (add_SNo_eps_Lt x HxS 0 H0omega).

We prove the intermediate claim Hxme0ltx: a0 < x.

An exact proof term for the current goal is (add_SNo_minus_Lt1b x e0 x HxS He0S HxS Hxlt).

We prove the intermediate claim Hax: Rlt a0 x.

An exact proof term for the current goal is (RltI a0 x HaR HxR Hxme0ltx).

We prove the intermediate claim HpropI: Rlt a0 x ∧ Rlt x b.

Apply andI to the current goal.

An exact proof term for the current goal is Hax.

An exact proof term for the current goal is Hxb.

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

We prove the intermediate claim HISubU: I ⊆ U.

Let y be given.

Assume HyI.

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ Rlt a0 y0 ∧ Rlt y0 b) y HyI).

We prove the intermediate claim HyProp: Rlt a0 y ∧ Rlt y b.

An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt a0 y0 ∧ Rlt y0 b) y HyI).

We prove the intermediate claim Hyb: Rlt y b.

An exact proof term for the current goal is (andER (Rlt a0 y) (Rlt y b) HyProp).

An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt y0 b) y HyR Hyb).

We use I to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HIStd.

Apply andI to the current goal.

An exact proof term for the current goal is HxInI.

An exact proof term for the current goal is HISubU.