We will prove rational_open_intervals_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ rational_open_intervals_basis, x ∈ b) ∧ (∀b1 ∈ rational_open_intervals_basis, ∀b2 ∈ rational_open_intervals_basis, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).

Apply andI to the current goal.

We will prove rational_open_intervals_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ rational_open_intervals_basis, x ∈ b).

Apply andI to the current goal.

We will prove rational_open_intervals_basis ⊆ 𝒫 R.

Let b be given.

Assume Hb: b ∈ rational_open_intervals_basis.

We will prove b ∈ 𝒫 R.

Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) b Hb (b ∈ 𝒫 R)) to the current goal.

Let q1 be given.

Assume Hq1 Hbq1.

Apply (ReplE_impred rational_numbers (λq2 : set ⇒ open_interval q1 q2) b Hbq1 (b ∈ 𝒫 R)) to the current goal.

Let q2 be given.

Assume Hq2 Heq.

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

An exact proof term for the current goal is (PowerI R (open_interval q1 q2) (open_interval_Subq_R q1 q2)).

Let x be given.

Assume HxR.

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

Set b0 to be the term add_SNo x 1.

We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.

An exact proof term for the current goal is (real_minus_SNo 1 real_1).

We prove the intermediate claim Ha0R: a0 ∈ R.

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

We prove the intermediate claim Hb0R: b0 ∈ R.

An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).

We prove the intermediate claim HxInI: x ∈ open_interval a0 b0.

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

We prove the intermediate claim HexRat: ∃q1 ∈ rational_numbers, ∃q2 ∈ rational_numbers, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a0 b0.

An exact proof term for the current goal is (rational_interval_refines_real_interval a0 b0 x Ha0R Hb0R HxR HxInI).

Apply HexRat to the current goal.

Let q1 be given.

Assume Hq1pair.

Apply Hq1pair to the current goal.

Assume Hq1: q1 ∈ rational_numbers.

Assume Hexq2: ∃q2 ∈ rational_numbers, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a0 b0.

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2pair.

Apply Hq2pair to the current goal.

Assume Hq2: q2 ∈ rational_numbers.

Assume HxInQ: x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a0 b0.

We prove the intermediate claim HxInQint: x ∈ open_interval q1 q2.

An exact proof term for the current goal is (andEL (x ∈ open_interval q1 q2) (open_interval q1 q2 ⊆ open_interval a0 b0) HxInQ).

We use (open_interval q1 q2) to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim Hq2fam: open_interval q1 q2 ∈ {open_interval q1 q2'|q2' ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λq2' : set ⇒ open_interval q1 q2') q2 Hq2).

An exact proof term for the current goal is (famunionI rational_numbers (λq1' : set ⇒ {open_interval q1' q2'|q2' ∈ rational_numbers}) q1 (open_interval q1 q2) Hq1 Hq2fam).

An exact proof term for the current goal is HxInQint.

Let b1 be given.

Assume Hb1.

Let b2 be given.

Assume Hb2.

Let x be given.

Assume Hx1 Hx2.

We will prove ∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.

We prove the intermediate claim Hexq1: ∃q1 ∈ rational_numbers, b1 ∈ {open_interval q1 q2|q2 ∈ rational_numbers}.

An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) b1 Hb1).

Apply Hexq1 to the current goal.

Let q1 be given.

Assume Hq1pair.

Apply Hq1pair to the current goal.

Assume Hq1Q: q1 ∈ rational_numbers.

Assume Hb1fam: b1 ∈ {open_interval q1 q2|q2 ∈ rational_numbers}.

We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, b1 = open_interval q1 q2.

An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ open_interval q1 q2) b1 Hb1fam).

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2pair.

Apply Hq2pair to the current goal.

Assume Hq2Q: q2 ∈ rational_numbers.

Assume Hb1eq: b1 = open_interval q1 q2.

We prove the intermediate claim Hexr1: ∃r1 ∈ rational_numbers, b2 ∈ {open_interval r1 r2|r2 ∈ rational_numbers}.

An exact proof term for the current goal is (famunionE rational_numbers (λr1 : set ⇒ {open_interval r1 r2|r2 ∈ rational_numbers}) b2 Hb2).

Apply Hexr1 to the current goal.

Let r1 be given.

Assume Hr1pair.

Apply Hr1pair to the current goal.

Assume Hr1Q: r1 ∈ rational_numbers.

Assume Hb2fam: b2 ∈ {open_interval r1 r2|r2 ∈ rational_numbers}.

We prove the intermediate claim Hexr2: ∃r2 ∈ rational_numbers, b2 = open_interval r1 r2.

An exact proof term for the current goal is (ReplE rational_numbers (λr2 : set ⇒ open_interval r1 r2) b2 Hb2fam).

Apply Hexr2 to the current goal.

Let r2 be given.

Assume Hr2pair.

Apply Hr2pair to the current goal.

Assume Hr2Q: r2 ∈ rational_numbers.

Assume Hb2eq: b2 = open_interval r1 r2.

We prove the intermediate claim HxIn1: x ∈ open_interval q1 q2.

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

An exact proof term for the current goal is Hx1.

We prove the intermediate claim HxIn2: x ∈ open_interval r1 r2.

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

An exact proof term for the current goal is Hx2.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) x HxIn1).

We prove the intermediate claim HxProp1: Rlt q1 x ∧ Rlt x q2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) x HxIn1).

We prove the intermediate claim HxProp2: Rlt r1 x ∧ Rlt x r2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) x HxIn2).

We prove the intermediate claim Hq1x: Rlt q1 x.

An exact proof term for the current goal is (andEL (Rlt q1 x) (Rlt x q2) HxProp1).

We prove the intermediate claim Hxq2: Rlt x q2.

An exact proof term for the current goal is (andER (Rlt q1 x) (Rlt x q2) HxProp1).

We prove the intermediate claim Hr1x: Rlt r1 x.

An exact proof term for the current goal is (andEL (Rlt r1 x) (Rlt x r2) HxProp2).

We prove the intermediate claim Hxr2: Rlt x r2.

An exact proof term for the current goal is (andER (Rlt r1 x) (Rlt x r2) HxProp2).

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 Hq2R: q2 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).

We prove the intermediate claim Hr1R: r1 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R r1 Hr1Q).

We prove the intermediate claim Hr2R: r2 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R r2 Hr2Q).

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 Hq2S: SNo q2.

An exact proof term for the current goal is (real_SNo q2 Hq2R).

We prove the intermediate claim Hr1S: SNo r1.

An exact proof term for the current goal is (real_SNo r1 Hr1R).

We prove the intermediate claim Hr2S: SNo r2.

An exact proof term for the current goal is (real_SNo r2 Hr2R).

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 Hq1xlt: q1 < x.

An exact proof term for the current goal is (RltE_lt q1 x Hq1x).

We prove the intermediate claim Hr1xlt: r1 < x.

An exact proof term for the current goal is (RltE_lt r1 x Hr1x).

We prove the intermediate claim Hxq2lt: x < q2.

An exact proof term for the current goal is (RltE_lt x q2 Hxq2).

We prove the intermediate claim Hxr2lt: x < r2.

An exact proof term for the current goal is (RltE_lt x r2 Hxr2).

Apply (SNoLt_trichotomy_or_impred q1 r1 Hq1S Hr1S (∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Assume Hq1lt: q1 < r1.

Apply (SNoLt_trichotomy_or_impred q2 r2 Hq2S Hr2S (∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Assume Hq2lt: q2 < r2.

Set I3 to be the term open_interval r1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval r1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval r1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) r1 I3 Hr1Q HI3fam).

Apply andI to the current goal.

We prove the intermediate claim Hr1xRlt: Rlt r1 x.

An exact proof term for the current goal is Hr1x.

We prove the intermediate claim Hxq2Rlt: Rlt x q2.

An exact proof term for the current goal is Hxq2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) x HxR (andI (Rlt r1 x) (Rlt x q2) Hr1xRlt Hxq2Rlt)).

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) y HyI3).

We prove the intermediate claim HyProp: Rlt r1 y ∧ Rlt y q2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) y HyI3).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (andEL (Rlt r1 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 r1 y) (Rlt y q2) HyProp).

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 Hr1ylt: r1 < y.

An exact proof term for the current goal is (RltE_lt r1 y Hr1y).

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 Hyr2lt: y < r2.

An exact proof term for the current goal is (SNoLt_tra y q2 r2 HyS Hq2S Hr2S Hyq2lt Hq2lt).

We prove the intermediate claim Hyr2: Rlt y r2.

An exact proof term for the current goal is (RltI y r2 HyR Hr2R Hyr2lt).

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

We prove the intermediate claim Hq1ylt: q1 < y.

An exact proof term for the current goal is (SNoLt_tra q1 r1 y Hq1S Hr1S HyS Hq1lt Hr1ylt).

We prove the intermediate claim Hq1y: Rlt q1 y.

An exact proof term for the current goal is (RltI q1 y Hq1R HyR Hq1ylt).

We prove the intermediate claim HyIn1: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hq1y Hyq2)).

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyIn1.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hq2eq: q2 = r2.

Set I3 to be the term open_interval r1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval r1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval r1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) r1 I3 Hr1Q HI3fam).

Apply andI to the current goal.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) x HxR (andI (Rlt r1 x) (Rlt x q2) Hr1x Hxq2)).

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) y HyI3).

We prove the intermediate claim HyProp: Rlt r1 y ∧ Rlt y q2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt r1 z ∧ Rlt z q2) y HyI3).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (andEL (Rlt r1 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 r1 y) (Rlt y q2) HyProp).

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 Hr1ylt: r1 < y.

An exact proof term for the current goal is (RltE_lt r1 y Hr1y).

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 Hyr2: Rlt y r2.

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

An exact proof term for the current goal is Hyq2.

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

We prove the intermediate claim Hq1ylt: q1 < y.

An exact proof term for the current goal is (SNoLt_tra q1 r1 y Hq1S Hr1S HyS Hq1lt Hr1ylt).

We prove the intermediate claim Hq1y: Rlt q1 y.

An exact proof term for the current goal is (RltI q1 y Hq1R HyR Hq1ylt).

We prove the intermediate claim HyIn1: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hq1y Hyq2)).

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyIn1.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hr2lt: r2 < q2.

Set I3 to be the term open_interval r1 r2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval r1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval r1 qq) r2 Hr2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) r1 I3 Hr1Q HI3fam).

Apply andI to the current goal.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) x HxR (andI (Rlt r1 x) (Rlt x r2) Hr1x Hxr2)).

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyI3).

We prove the intermediate claim HyProp: Rlt r1 y ∧ Rlt y r2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyI3).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (andEL (Rlt r1 y) (Rlt y r2) HyProp).

We prove the intermediate claim Hyr2: Rlt y r2.

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

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 Hr1ylt: r1 < y.

An exact proof term for the current goal is (RltE_lt r1 y Hr1y).

We prove the intermediate claim Hyr2lt: y < r2.

An exact proof term for the current goal is (RltE_lt y r2 Hyr2).

We prove the intermediate claim Hyq2lt: y < q2.

An exact proof term for the current goal is (SNoLt_tra y r2 q2 HyS Hr2S Hq2S Hyr2lt Hr2lt).

We prove the intermediate claim Hyq2: Rlt y q2.

An exact proof term for the current goal is (RltI y q2 HyR Hq2R Hyq2lt).

We prove the intermediate claim Hq1ylt: q1 < y.

An exact proof term for the current goal is (SNoLt_tra q1 r1 y Hq1S Hr1S HyS Hq1lt Hr1ylt).

We prove the intermediate claim Hq1y: Rlt q1 y.

An exact proof term for the current goal is (RltI q1 y Hq1R HyR Hq1ylt).

We prove the intermediate claim HyIn1: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hq1y Hyq2)).

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyIn1.

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hq1eq: q1 = r1.

Apply (SNoLt_trichotomy_or_impred q2 r2 Hq2S Hr2S (∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Assume Hq2lt: q2 < r2.

Set I3 to be the term open_interval q1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

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

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyI3.

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

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

We prove the intermediate claim Hqy: 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 HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

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 Hyr2lt: y < r2.

An exact proof term for the current goal is (SNoLt_tra y q2 r2 HyS Hq2S Hr2S Hyq2lt Hq2lt).

We prove the intermediate claim Hyr2: Rlt y r2.

An exact proof term for the current goal is (RltI y r2 HyR Hr2R Hyr2lt).

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

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

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) y HyR (andI (Rlt q1 y) (Rlt y r2) Hqy Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hq2eq: q2 = r2.

Set I3 to be the term open_interval q1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

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

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyI3.

We prove the intermediate claim Hyb2: y ∈ b2.

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

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

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

An exact proof term for the current goal is HyI3.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hr2lt: r2 < q2.

Set I3 to be the term open_interval q1 r2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) r2 Hr2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

Apply andI to the current goal.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) x HxR (andI (Rlt q1 x) (Rlt x r2) Hq1x Hxr2)).

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

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 r2) y HyI3).

We prove the intermediate claim HyProp: Rlt q1 y ∧ Rlt y r2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) y HyI3).

We prove the intermediate claim Hq1y: Rlt q1 y.

An exact proof term for the current goal is (andEL (Rlt q1 y) (Rlt y r2) HyProp).

We prove the intermediate claim Hyr2: Rlt y r2.

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

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 Hyr2lt: y < r2.

An exact proof term for the current goal is (RltE_lt y r2 Hyr2).

We prove the intermediate claim Hyq2lt: y < q2.

An exact proof term for the current goal is (SNoLt_tra y r2 q2 HyS Hr2S Hq2S Hyr2lt Hr2lt).

We prove the intermediate claim Hyq2: Rlt y q2.

An exact proof term for the current goal is (RltI y q2 HyR Hq2R Hyq2lt).

We prove the intermediate claim HyIn1: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hq1y Hyq2)).

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyIn1.

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

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

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) y HyR (andI (Rlt q1 y) (Rlt y r2) Hq1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hr1lt: r1 < q1.

Apply (SNoLt_trichotomy_or_impred q2 r2 Hq2S Hr2S (∃b3 ∈ rational_open_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Assume Hq2lt: q2 < r2.

Set I3 to be the term open_interval q1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

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

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyI3.

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

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

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 HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

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 Hr1ylt: r1 < y.

An exact proof term for the current goal is (SNoLt_tra r1 q1 y Hr1S Hq1S HyS Hr1lt Hq1ylt).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (RltI r1 y Hr1R HyR Hr1ylt).

We prove the intermediate claim Hyr2lt: y < r2.

An exact proof term for the current goal is (SNoLt_tra y q2 r2 HyS Hq2S Hr2S Hyq2lt Hq2lt).

We prove the intermediate claim Hyr2: Rlt y r2.

An exact proof term for the current goal is (RltI y r2 HyR Hr2R Hyr2lt).

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hq2eq: q2 = r2.

Set I3 to be the term open_interval q1 q2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) q2 Hq2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

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

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyI3.

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

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

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 HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

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 Hr1ylt: r1 < y.

An exact proof term for the current goal is (SNoLt_tra r1 q1 y Hr1S Hq1S HyS Hr1lt Hq1ylt).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (RltI r1 y Hr1R HyR Hr1ylt).

We prove the intermediate claim Hyr2: Rlt y r2.

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

An exact proof term for the current goal is Hyq2.

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

Assume Hr2lt: r2 < q2.

Set I3 to be the term open_interval q1 r2.

We use I3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HI3fam: I3 ∈ {open_interval q1 qq|qq ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ open_interval q1 qq) r2 Hr2Q).

An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {open_interval aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).

Apply andI to the current goal.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) x HxR (andI (Rlt q1 x) (Rlt x r2) Hq1x Hxr2)).

Let y be given.

Assume HyI3: y ∈ I3.

We will prove y ∈ b1 ∩ b2.

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 r2) y HyI3).

We prove the intermediate claim HyProp: Rlt q1 y ∧ Rlt y r2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z r2) y HyI3).

We prove the intermediate claim Hq1y: Rlt q1 y.

An exact proof term for the current goal is (andEL (Rlt q1 y) (Rlt y r2) HyProp).

We prove the intermediate claim Hyr2: Rlt y r2.

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

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 Hq1ylt: q1 < y.

An exact proof term for the current goal is (RltE_lt q1 y Hq1y).

We prove the intermediate claim Hyr2lt: y < r2.

An exact proof term for the current goal is (RltE_lt y r2 Hyr2).

We prove the intermediate claim Hyq2lt: y < q2.

An exact proof term for the current goal is (SNoLt_tra y r2 q2 HyS Hr2S Hq2S Hyr2lt Hr2lt).

We prove the intermediate claim Hyq2: Rlt y q2.

An exact proof term for the current goal is (RltI y q2 HyR Hq2R Hyq2lt).

We prove the intermediate claim HyIn1: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hq1y Hyq2)).

We prove the intermediate claim Hyb1: y ∈ b1.

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

An exact proof term for the current goal is HyIn1.

We prove the intermediate claim Hr1ylt: r1 < y.

An exact proof term for the current goal is (SNoLt_tra r1 q1 y Hr1S Hq1S HyS Hr1lt Hq1ylt).

We prove the intermediate claim Hr1y: Rlt r1 y.

An exact proof term for the current goal is (RltI r1 y Hr1R HyR Hr1ylt).

We prove the intermediate claim HyIn2: y ∈ open_interval r1 r2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt r1 z ∧ Rlt z r2) y HyR (andI (Rlt r1 y) (Rlt y r2) Hr1y Hyr2)).

We prove the intermediate claim Hyb2: y ∈ b2.

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

An exact proof term for the current goal is HyIn2.

An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).

We will prove generated_topology R rational_open_intervals_basis = R_standard_topology.

Apply set_ext to the current goal.

Let U be given.

Assume HU: U ∈ generated_topology R rational_open_intervals_basis.

We will prove U ∈ R_standard_topology.

We prove the intermediate claim HUpow: U ∈ 𝒫 R.

An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ rational_open_intervals_basis, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ rational_open_intervals_basis, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ rational_open_intervals_basis, x0 ∈ b ∧ b ⊆ U0) U HU).

We will prove U ∈ generated_topology R R_standard_basis.

We will prove U ∈ {U0 ∈ 𝒫 R|∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0}.

We prove the intermediate claim HUstdprop: ∀x0 ∈ U, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U.

Let x be given.

Assume HxU: x ∈ U.

Apply (HUprop x HxU) to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim HbB: b ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (andEL (b ∈ rational_open_intervals_basis) (x ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ rational_open_intervals_basis) (x ∈ b ∧ b ⊆ U) Hbpair).

We prove the intermediate claim Hxb: x ∈ b.

An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbStd: b ∈ R_standard_basis.

An exact proof term for the current goal is (rational_open_intervals_basis_Subq_R_standard_basis b HbB).

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbStd.

Apply andI to the current goal.

An exact proof term for the current goal is Hxb.

An exact proof term for the current goal is HbsubU.

An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HUpow HUstdprop).

Let U be given.

Assume HU: U ∈ R_standard_topology.

We will prove U ∈ generated_topology R rational_open_intervals_basis.

We prove the intermediate claim HUpow: U ∈ 𝒫 R.

An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim HUsubR: U ⊆ R.

An exact proof term for the current goal is (PowerE R U HUpow).

We will prove U ∈ {U0 ∈ 𝒫 R|∀x0 ∈ U0, ∃b ∈ rational_open_intervals_basis, x0 ∈ b ∧ b ⊆ U0}.

Apply SepI to the current goal.

An exact proof term for the current goal is HUpow.

Let x be given.

Assume HxU: x ∈ U.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (HUsubR x HxU).

Apply (HUprop x HxU) to the current goal.

Let I be given.

Assume HIpair.

We prove the intermediate claim HIStd: I ∈ R_standard_basis.

An exact proof term for the current goal is (andEL (I ∈ R_standard_basis) (x ∈ I ∧ I ⊆ U) HIpair).

We prove the intermediate claim HIprop: x ∈ I ∧ I ⊆ U.

An exact proof term for the current goal is (andER (I ∈ R_standard_basis) (x ∈ I ∧ I ⊆ U) HIpair).

We prove the intermediate claim HxI: x ∈ I.

An exact proof term for the current goal is (andEL (x ∈ I) (I ⊆ U) HIprop).

We prove the intermediate claim HIsubU: I ⊆ U.

An exact proof term for the current goal is (andER (x ∈ I) (I ⊆ U) HIprop).

We prove the intermediate claim Hexa: ∃a ∈ R, I ∈ {open_interval a b|b ∈ R}.

An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) I HIStd).

Apply Hexa to the current goal.

Let a be given.

Assume Hapair.

Apply Hapair to the current goal.

Assume HaR: a ∈ R.

Assume HIfam: I ∈ {open_interval a b|b ∈ R}.

We prove the intermediate claim Hexb: ∃b ∈ R, I = open_interval a b.

An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0) I HIfam).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

Apply Hbpair to the current goal.

Assume HbR: b ∈ R.

Assume HIeq: I = open_interval a b.

We prove the intermediate claim HxInab: x ∈ open_interval a b.

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

An exact proof term for the current goal is HxI.

We prove the intermediate claim HexRat: ∃q1 ∈ rational_numbers, ∃q2 ∈ rational_numbers, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

An exact proof term for the current goal is (rational_interval_refines_real_interval a b x HaR HbR HxR HxInab).

Apply HexRat to the current goal.

Let q1 be given.

Assume Hq1pair.

Apply Hq1pair to the current goal.

Assume Hq1Q: q1 ∈ rational_numbers.

Assume Hexq2: ∃q2 ∈ rational_numbers, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2pair.

Apply Hq2pair to the current goal.

Assume Hq2Q: q2 ∈ rational_numbers.

Assume HxInQ: x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

We prove the intermediate claim HxInQint: x ∈ open_interval q1 q2.

An exact proof term for the current goal is (andEL (x ∈ open_interval q1 q2) (open_interval q1 q2 ⊆ open_interval a b) HxInQ).

We prove the intermediate claim HQsub: open_interval q1 q2 ⊆ open_interval a b.

An exact proof term for the current goal is (andER (x ∈ open_interval q1 q2) (open_interval q1 q2 ⊆ open_interval a b) HxInQ).

We prove the intermediate claim HabsubU: open_interval a b ⊆ U.

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

An exact proof term for the current goal is HIsubU.

We prove the intermediate claim HQsubU: open_interval q1 q2 ⊆ U.

An exact proof term for the current goal is (Subq_tra (open_interval q1 q2) (open_interval a b) U HQsub HabsubU).

We prove the intermediate claim Hq2fam: open_interval q1 q2 ∈ {open_interval q1 q2'|q2' ∈ rational_numbers}.

An exact proof term for the current goal is (ReplI rational_numbers (λq2' : set ⇒ open_interval q1 q2') q2 Hq2Q).

We prove the intermediate claim HbInB: open_interval q1 q2 ∈ rational_open_intervals_basis.

An exact proof term for the current goal is (famunionI rational_numbers (λq1' : set ⇒ {open_interval q1' q2'|q2' ∈ rational_numbers}) q1 (open_interval q1 q2) Hq1Q Hq2fam).

We use (open_interval q1 q2) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbInB.

Apply andI to the current goal.

An exact proof term for the current goal is HxInQint.

An exact proof term for the current goal is HQsubU.