Assume HbU: b ∈ Bold.

Apply (binunionE' (A ∪ B) C b (∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ b)) to the current goal.

Assume HbAB: b ∈ (A ∪ B).

Apply (binunionE' A B b (∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ b)) to the current goal.

Assume HbA: b ∈ A.

We prove the intermediate claim Hex: ∃a0 ∈ R, ∃b0 ∈ R, b = {y ∈ R|order_rel R a0 y ∧ order_rel R y b0}.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, ∃b0 ∈ R, I0 = {y ∈ R|order_rel R a0 y ∧ order_rel R y b0}) b HbA).

Apply Hex to the current goal.

Let a0 be given.

Assume Ha0core.

Apply Ha0core to the current goal.

Assume Ha0R: a0 ∈ R.

Assume Hexb0: ∃b0 ∈ R, b = {y ∈ R|order_rel R a0 y ∧ order_rel R y b0}.

Apply Hexb0 to the current goal.

Let b0 be given.

Assume Hb0core.

Apply Hb0core to the current goal.

Assume Hb0R: b0 ∈ R.

Assume Hbeq: b = {y ∈ R|order_rel R a0 y ∧ order_rel R y b0}.

Set I to be the term open_interval a0 b0.

We prove the intermediate claim HIinStdBasis: 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) b0 Hb0R).

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

We prove the intermediate claim HxInSet: x ∈ {y ∈ R|order_rel R a0 y ∧ order_rel R y b0}.

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is Hxb.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λy : set ⇒ order_rel R a0 y ∧ order_rel R y b0) x HxInSet).

We prove the intermediate claim Hxconj: order_rel R a0 x ∧ order_rel R x b0.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R a0 y ∧ order_rel R y b0) x HxInSet).

We prove the intermediate claim Hax: order_rel R a0 x.

An exact proof term for the current goal is (andEL (order_rel R a0 x) (order_rel R x b0) Hxconj).

We prove the intermediate claim Hxb0: order_rel R x b0.

An exact proof term for the current goal is (andER (order_rel R a0 x) (order_rel R x b0) Hxconj).

We prove the intermediate claim Haxlt: Rlt a0 x.

An exact proof term for the current goal is (order_rel_R_implies_Rlt a0 x Hax).

We prove the intermediate claim Hxblt: Rlt x b0.

An exact proof term for the current goal is (order_rel_R_implies_Rlt x b0 Hxb0).

We prove the intermediate claim HxI: x ∈ I.

An exact proof term for the current goal is (SepI R (λy : set ⇒ Rlt a0 y ∧ Rlt y b0) x HxR (andI (Rlt a0 x) (Rlt x b0) Haxlt Hxblt)).

We prove the intermediate claim HIsubB: I ⊆ b.

Let y be given.

Assume HyI: y ∈ I.

We will prove y ∈ b.

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 b0) y HyI).

We prove the intermediate claim Hyconj: Rlt a0 y ∧ Rlt y b0.

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

We prove the intermediate claim Hay: Rlt a0 y.

An exact proof term for the current goal is (andEL (Rlt a0 y) (Rlt y b0) Hyconj).

We prove the intermediate claim Hyb: Rlt y b0.

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

We prove the intermediate claim Hayrel: order_rel R a0 y.

An exact proof term for the current goal is (Rlt_implies_order_rel_R a0 y Hay).

We prove the intermediate claim Hybrel: order_rel R y b0.

An exact proof term for the current goal is (Rlt_implies_order_rel_R y b0 Hyb).

We prove the intermediate claim HySet: y ∈ {z ∈ R|order_rel R a0 z ∧ order_rel R z b0}.

An exact proof term for the current goal is (SepI R (λz : set ⇒ order_rel R a0 z ∧ order_rel R z b0) y HyR (andI (order_rel R a0 y) (order_rel R y b0) Hayrel Hybrel)).

rewrite the current goal using Hbeq (from left to right).

An exact proof term for the current goal is HySet.

We use I to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HIinStdBasis.

Apply andI to the current goal.

An exact proof term for the current goal is HxI.

An exact proof term for the current goal is HIsubB.

Assume HbB: b ∈ B.

We prove the intermediate claim Hex: ∃b0 ∈ R, b = {y ∈ R|order_rel R y b0}.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = {y ∈ R|order_rel R y b0}) b HbB).

Apply Hex to the current goal.

Let b0 be given.

Assume Hb0core.

Apply Hb0core to the current goal.

Assume Hb0R: b0 ∈ R.

Assume Hbeq: b = {y ∈ R|order_rel R y b0}.

We prove the intermediate claim HxInSet: x ∈ {y ∈ R|order_rel R y b0}.

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is Hxb.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λy : set ⇒ order_rel R y b0) x HxInSet).

We prove the intermediate claim Hrel: order_rel R x b0.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R y b0) x HxInSet).

We prove the intermediate claim Hxltb0: Rlt x b0.

An exact proof term for the current goal is (order_rel_R_implies_Rlt x b0 Hrel).

We prove the intermediate claim Hxpm: x ∈ open_interval (add_SNo x (minus_SNo 1)) (add_SNo x 1).

An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 x HxR).

Set a1 to be the term add_SNo x (minus_SNo 1).

Set c1 to be the term add_SNo x 1.

We prove the intermediate claim Ha1R: a1 ∈ R.

An exact proof term for the current goal is (open_interval_left_in_R a1 c1 x Hxpm).

We prove the intermediate claim Hleft: Rlt a1 x.

We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x c1.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ Rlt a1 y ∧ Rlt y c1) x Hxpm).

An exact proof term for the current goal is (andEL (Rlt a1 x) (Rlt x c1) Hconj).

Set I to be the term open_interval a1 b0.

We prove the intermediate claim HIinStdBasis: I ∈ R_standard_basis.

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

An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) b0 Hb0R).

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

We prove the intermediate claim HxI: x ∈ I.

An exact proof term for the current goal is (SepI R (λy : set ⇒ Rlt a1 y ∧ Rlt y b0) x HxR (andI (Rlt a1 x) (Rlt x b0) Hleft Hxltb0)).

We prove the intermediate claim HIsubB: I ⊆ b.

Let y be given.

Assume HyI: y ∈ I.

We will prove y ∈ b.

We prove the intermediate claim HyR: y ∈ R.

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

We prove the intermediate claim Hyconj: Rlt a1 y ∧ Rlt y b0.

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

We prove the intermediate claim Hyb: Rlt y b0.

An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y b0) Hyconj).

We prove the intermediate claim Hyrel: order_rel R y b0.

An exact proof term for the current goal is (Rlt_implies_order_rel_R y b0 Hyb).

We prove the intermediate claim HySet: y ∈ {z ∈ R|order_rel R z b0}.

An exact proof term for the current goal is (SepI R (λz : set ⇒ order_rel R z b0) y HyR Hyrel).

rewrite the current goal using Hbeq (from left to right).

An exact proof term for the current goal is HySet.

We use I to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HIinStdBasis.

Apply andI to the current goal.

An exact proof term for the current goal is HxI.

An exact proof term for the current goal is HIsubB.

An exact proof term for the current goal is HbAB.

Assume HbC: b ∈ C.

We prove the intermediate claim Hex: ∃a0 ∈ R, b = {y ∈ R|order_rel R a0 y}.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = {y ∈ R|order_rel R a0 y}) b HbC).

Apply Hex to the current goal.

Let a0 be given.

Assume Ha0core.

Apply Ha0core to the current goal.

Assume Ha0R: a0 ∈ R.

Assume Hbeq: b = {y ∈ R|order_rel R a0 y}.

We prove the intermediate claim HxInSet: x ∈ {y ∈ R|order_rel R a0 y}.

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is Hxb.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λy : set ⇒ order_rel R a0 y) x HxInSet).

We prove the intermediate claim Hrel: order_rel R a0 x.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ order_rel R a0 y) x HxInSet).

We prove the intermediate claim Ha0ltx: Rlt a0 x.

An exact proof term for the current goal is (order_rel_R_implies_Rlt a0 x Hrel).

We prove the intermediate claim Hxpm: x ∈ open_interval (add_SNo x (minus_SNo 1)) (add_SNo x 1).

An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 x HxR).

Set a1 to be the term add_SNo x (minus_SNo 1).

Set c1 to be the term add_SNo x 1.

We prove the intermediate claim Hright: Rlt x c1.

We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x c1.

An exact proof term for the current goal is (SepE2 R (λy : set ⇒ Rlt a1 y ∧ Rlt y c1) x Hxpm).

An exact proof term for the current goal is (andER (Rlt a1 x) (Rlt x c1) Hconj).

We prove the intermediate claim Hc1R: c1 ∈ R.

An exact proof term for the current goal is (open_interval_right_in_R a1 c1 x Hxpm).

Set I to be the term open_interval a0 c1.

We prove the intermediate claim HIinStdBasis: 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) c1 Hc1R).

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

We prove the intermediate claim HxI: x ∈ I.

An exact proof term for the current goal is (SepI R (λy : set ⇒ Rlt a0 y ∧ Rlt y c1) x HxR (andI (Rlt a0 x) (Rlt x c1) Ha0ltx Hright)).

We prove the intermediate claim HIsubB: I ⊆ b.

Let y be given.

Assume HyI: y ∈ I.

We will prove y ∈ b.

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 c1) y HyI).

We prove the intermediate claim Hyconj: Rlt a0 y ∧ Rlt y c1.

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

We prove the intermediate claim Hay: Rlt a0 y.

An exact proof term for the current goal is (andEL (Rlt a0 y) (Rlt y c1) Hyconj).

We prove the intermediate claim Hayrel: order_rel R a0 y.

An exact proof term for the current goal is (Rlt_implies_order_rel_R a0 y Hay).

We prove the intermediate claim HySet: y ∈ {z ∈ R|order_rel R a0 z}.

An exact proof term for the current goal is (SepI R (λz : set ⇒ order_rel R a0 z) y HyR Hayrel).

rewrite the current goal using Hbeq (from left to right).

An exact proof term for the current goal is HySet.

We use I to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HIinStdBasis.

Apply andI to the current goal.

An exact proof term for the current goal is HxI.

An exact proof term for the current goal is HIsubB.

An exact proof term for the current goal is HbU.