We will prove basis_on R rational_halfopen_intervals_basis ∧ generated_topology R rational_halfopen_intervals_basis ≠ R_lower_limit_topology.
Apply andI to the current goal.
We will prove rational_halfopen_intervals_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ rational_halfopen_intervals_basis, x ∈ b) ∧ (∀b1 ∈ rational_halfopen_intervals_basis, ∀b2 ∈ rational_halfopen_intervals_basis, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ rational_halfopen_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply andI to the current goal.
We will prove rational_halfopen_intervals_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ rational_halfopen_intervals_basis, x ∈ b).
Apply andI to the current goal.
We will prove rational_halfopen_intervals_basis ⊆ 𝒫 R.
Let b be given.
Assume Hb: b ∈ rational_halfopen_intervals_basis.
We will prove b ∈ 𝒫 R.
Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {halfopen_interval_left 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 ⇒ halfopen_interval_left 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 (halfopen_interval_left q1 q2) (halfopen_interval_left_Subq_R q1 q2)).
We will prove ∀x ∈ R, ∃b ∈ rational_halfopen_intervals_basis, x ∈ b.
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 HxInab: 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 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 a0 b0.
Apply Hexq2 to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume Hxpair: x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a0 b0.
We prove the intermediate claim HxInQ: 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) Hxpair).
We prove the intermediate claim HxInQprop: 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 HxInQ).
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) HxInQprop).
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) HxInQprop).
Set I to be the term halfopen_interval_left q1 q2.
We prove the intermediate claim HIinFam: I ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
We prove the intermediate claim HIinB: I ∈ rational_halfopen_intervals_basis.
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I Hq1Q HIinFam).
We prove the intermediate claim Hnxq1: ¬ (Rlt x q1).
Assume Hxq1: Rlt x q1.
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 Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
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 Hxq1lt: x < q1.
An exact proof term for the current goal is (RltE_lt x q1 Hxq1).
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 Hxxlt: x < x.
An exact proof term for the current goal is (SNoLt_tra x q1 x HxS Hq1S HxS Hxq1lt Hq1xlt).
An exact proof term for the current goal is ((SNoLt_irref x) Hxxlt).
We prove the intermediate claim HxInI: x ∈ I.
We prove the intermediate claim Hconj: ¬ (Rlt x q1) ∧ Rlt x q2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxq1.
An exact proof term for the current goal is Hxq2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) x HxR Hconj).
We use I to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HIinB.
An exact proof term for the current goal is HxInI.
Let b1 be given.
Assume Hb1.
Let b2 be given.
Assume Hb2.
Let x be given.
Assume Hx1 Hx2.
We will prove ∃b3 ∈ rational_halfopen_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hexq1: ∃q1 ∈ rational_numbers, b1 ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {halfopen_interval_left 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 ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, b1 = halfopen_interval_left q1 q2.
An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ halfopen_interval_left 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 = halfopen_interval_left q1 q2.
We prove the intermediate claim Hexr1: ∃r1 ∈ rational_numbers, b2 ∈ {halfopen_interval_left r1 r2|r2 ∈ rational_numbers}.
An exact proof term for the current goal is (famunionE rational_numbers (λr1 : set ⇒ {halfopen_interval_left 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 ∈ {halfopen_interval_left r1 r2|r2 ∈ rational_numbers}.
We prove the intermediate claim Hexr2: ∃r2 ∈ rational_numbers, b2 = halfopen_interval_left r1 r2.
An exact proof term for the current goal is (ReplE rational_numbers (λr2 : set ⇒ halfopen_interval_left 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 = halfopen_interval_left r1 r2.
We prove the intermediate claim HxIn1: x ∈ halfopen_interval_left 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 ∈ halfopen_interval_left 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 z q1) ∧ Rlt z q2) x HxIn1).
We prove the intermediate claim HxProp1: ¬ (Rlt x q1) ∧ Rlt x q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) x HxIn1).
We prove the intermediate claim HxProp2: ¬ (Rlt x r1) ∧ Rlt x r2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) x HxIn2).
We prove the intermediate claim Hnxq1: ¬ (Rlt x q1).
An exact proof term for the current goal is (andEL (¬ (Rlt x q1)) (Rlt x q2) HxProp1).
We prove the intermediate claim Hxq2: Rlt x q2.
An exact proof term for the current goal is (andER (¬ (Rlt x q1)) (Rlt x q2) HxProp1).
We prove the intermediate claim Hnxr1: ¬ (Rlt x r1).
An exact proof term for the current goal is (andEL (¬ (Rlt x r1)) (Rlt x r2) HxProp2).
We prove the intermediate claim Hxr2: Rlt x r2.
An exact proof term for the current goal is (andER (¬ (Rlt x r1)) (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 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_halfopen_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_halfopen_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hq2lt: q2 < r2.
Set I3 to be the term halfopen_interval_left r1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left r1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left r1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) r1 I3 Hr1Q HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x r1) ∧ Rlt x q2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxr1.
An exact proof term for the current goal is Hxq2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z q2) x HxR Hconj).
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 z r1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y r1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim Hnyr1: ¬ (Rlt y r1).
An exact proof term for the current goal is (andEL (¬ (Rlt y r1)) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y r1)) (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 ∈ halfopen_interval_left r1 r2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y r1)) (Rlt y r2) Hnyr1 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 Hnyq1: ¬ (Rlt y q1).
Assume Hyq1: Rlt y q1.
We prove the intermediate claim Hyq1lt: y < q1.
An exact proof term for the current goal is (RltE_lt y q1 Hyq1).
We prove the intermediate claim Hyr1lt: y < r1.
An exact proof term for the current goal is (SNoLt_tra y q1 r1 HyS Hq1S Hr1S Hyq1lt Hq1lt).
We prove the intermediate claim Hyr1: Rlt y r1.
An exact proof term for the current goal is (RltI y r1 HyR Hr1R Hyr1lt).
An exact proof term for the current goal is (Hnyr1 Hyr1).
We prove the intermediate claim HyIn1: y ∈ halfopen_interval_left q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyR (andI (¬ (Rlt y q1)) (Rlt y q2) Hnyq1 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 halfopen_interval_left r1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left r1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left r1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left 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 z r1) ∧ Rlt z q2) x HxR (andI (¬ (Rlt x r1)) (Rlt x q2) Hnxr1 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 z r1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y r1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim Hnyr1: ¬ (Rlt y r1).
An exact proof term for the current goal is (andEL (¬ (Rlt y r1)) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y r1)) (Rlt y q2) HyProp).
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 ∈ halfopen_interval_left r1 r2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y r1)) (Rlt y r2) Hnyr1 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 Hnyq1: ¬ (Rlt y q1).
Assume Hyq1: Rlt y q1.
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 Hyq1lt: y < q1.
An exact proof term for the current goal is (RltE_lt y q1 Hyq1).
We prove the intermediate claim Hyr1lt: y < r1.
An exact proof term for the current goal is (SNoLt_tra y q1 r1 HyS Hq1S Hr1S Hyq1lt Hq1lt).
We prove the intermediate claim Hyr1: Rlt y r1.
An exact proof term for the current goal is (RltI y r1 HyR Hr1R Hyr1lt).
An exact proof term for the current goal is (Hnyr1 Hyr1).
We prove the intermediate claim HyIn1: y ∈ halfopen_interval_left q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyR (andI (¬ (Rlt y q1)) (Rlt y q2) Hnyq1 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 halfopen_interval_left r1 r2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left r1 rr|rr ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λrr : set ⇒ halfopen_interval_left r1 rr) r2 Hr2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) r1 I3 Hr1Q HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x r1) ∧ Rlt x r2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxr1.
An exact proof term for the current goal is Hxr2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) x HxR Hconj).
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 z r1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y r1) ∧ Rlt y r2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim Hnyr1: ¬ (Rlt y r1).
An exact proof term for the current goal is (andEL (¬ (Rlt y r1)) (Rlt y r2) HyProp).
We prove the intermediate claim Hyr2: Rlt y r2.
An exact proof term for the current goal is (andER (¬ (Rlt y r1)) (Rlt y r2) HyProp).
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 HyI3.
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 Hnyq1: ¬ (Rlt y q1).
Assume Hyq1: Rlt y q1.
We prove the intermediate claim Hyq1lt: y < q1.
An exact proof term for the current goal is (RltE_lt y q1 Hyq1).
We prove the intermediate claim Hyr1lt: y < r1.
An exact proof term for the current goal is (SNoLt_tra y q1 r1 HyS Hq1S Hr1S Hyq1lt Hq1lt).
We prove the intermediate claim Hyr1: Rlt y r1.
An exact proof term for the current goal is (RltI y r1 HyR Hr1R Hyr1lt).
An exact proof term for the current goal is (Hnyr1 Hyr1).
We prove the intermediate claim HyIn1: y ∈ halfopen_interval_left q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyR (andI (¬ (Rlt y q1)) (Rlt y q2) Hnyq1 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 Hq1eq: q1 = r1.
Apply (SNoLt_trichotomy_or_impred q2 r2 Hq2S Hr2S (∃b3 ∈ rational_halfopen_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hq2lt: q2 < r2.
Set I3 to be the term halfopen_interval_left q1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
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 z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y q1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (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 ∈ halfopen_interval_left r1 r2.
rewrite the current goal using Hq1eq (from right to left) at position 1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y q1)) (Rlt y r2) Hnyq1 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 halfopen_interval_left q1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
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 halfopen_interval_left q1 r2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 rr|rr ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λrr : set ⇒ halfopen_interval_left q1 rr) r2 Hr2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x q1) ∧ Rlt x r2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxq1.
An exact proof term for the current goal is Hxr2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) x HxR Hconj).
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 z q1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y q1) ∧ Rlt y r2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y r2) HyProp).
We prove the intermediate claim Hyr2: Rlt y r2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (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 ∈ halfopen_interval_left q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyR (andI (¬ (Rlt y q1)) (Rlt y q2) Hnyq1 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 ∈ halfopen_interval_left r1 r2.
rewrite the current goal using Hq1eq (from right to left) at position 1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y q1)) (Rlt y r2) Hnyq1 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_halfopen_intervals_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hq2lt: q2 < r2.
Set I3 to be the term halfopen_interval_left q1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
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 z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y q1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (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 Hnyr1: ¬ (Rlt y r1).
Assume Hyr1: Rlt y r1.
We prove the intermediate claim Hyr1lt: y < r1.
An exact proof term for the current goal is (RltE_lt y r1 Hyr1).
We prove the intermediate claim Hyq1lt: y < q1.
An exact proof term for the current goal is (SNoLt_tra y r1 q1 HyS Hr1S Hq1S Hyr1lt Hr1lt).
We prove the intermediate claim Hyq1: Rlt y q1.
An exact proof term for the current goal is (RltI y q1 HyR Hq1R Hyq1lt).
An exact proof term for the current goal is (Hnyq1 Hyq1).
We prove the intermediate claim HyIn2: y ∈ halfopen_interval_left r1 r2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y r1)) (Rlt y r2) Hnyr1 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 halfopen_interval_left q1 q2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 qq|qq ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λqq : set ⇒ halfopen_interval_left q1 qq) q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
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 z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y q1) ∧ Rlt y q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyI3).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y q2) HyProp).
We prove the intermediate claim Hyq2: Rlt y q2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (Rlt y q2) HyProp).
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 Hnyr1: ¬ (Rlt y r1).
Assume Hyr1: Rlt y r1.
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 Hyr1lt: y < r1.
An exact proof term for the current goal is (RltE_lt y r1 Hyr1).
We prove the intermediate claim Hyq1lt: y < q1.
An exact proof term for the current goal is (SNoLt_tra y r1 q1 HyS Hr1S Hq1S Hyr1lt Hr1lt).
We prove the intermediate claim Hyq1: Rlt y q1.
An exact proof term for the current goal is (RltI y q1 HyR Hq1R Hyq1lt).
An exact proof term for the current goal is (Hnyq1 Hyq1).
We prove the intermediate claim HyIn2: y ∈ halfopen_interval_left r1 r2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y r1)) (Rlt y r2) Hnyr1 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 halfopen_interval_left q1 r2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left q1 rr|rr ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λrr : set ⇒ halfopen_interval_left q1 rr) r2 Hr2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ rational_numbers}) q1 I3 Hq1Q HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x q1) ∧ Rlt x r2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxq1.
An exact proof term for the current goal is Hxr2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) x HxR Hconj).
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 z q1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim HyProp: ¬ (Rlt y q1) ∧ Rlt y r2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z r2) y HyI3).
We prove the intermediate claim Hnyq1: ¬ (Rlt y q1).
An exact proof term for the current goal is (andEL (¬ (Rlt y q1)) (Rlt y r2) HyProp).
We prove the intermediate claim Hyr2: Rlt y r2.
An exact proof term for the current goal is (andER (¬ (Rlt y q1)) (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 ∈ halfopen_interval_left q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) y HyR (andI (¬ (Rlt y q1)) (Rlt y q2) Hnyq1 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 Hnyr1: ¬ (Rlt y r1).
Assume Hyr1: Rlt y r1.
We prove the intermediate claim Hyr1lt: y < r1.
An exact proof term for the current goal is (RltE_lt y r1 Hyr1).
We prove the intermediate claim Hyq1lt: y < q1.
An exact proof term for the current goal is (SNoLt_tra y r1 q1 HyS Hr1S Hq1S Hyr1lt Hr1lt).
We prove the intermediate claim Hyq1: Rlt y q1.
An exact proof term for the current goal is (RltI y q1 HyR Hq1R Hyq1lt).
An exact proof term for the current goal is (Hnyq1 Hyq1).
We prove the intermediate claim HyIn2: y ∈ halfopen_interval_left r1 r2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z r1) ∧ Rlt z r2) y HyR (andI (¬ (Rlt y r1)) (Rlt y r2) Hnyr1 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 Heq: generated_topology R rational_halfopen_intervals_basis = R_lower_limit_topology.
Set a to be the term sqrt_SNo_nonneg 2.
Set U to be the term {x ∈ R|¬ (Rlt x a)}.
We prove the intermediate claim HaDiff: a ∈ R ∖ rational_numbers.
An exact proof term for the current goal is sqrt_2_irrational.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (setminusE1 R rational_numbers a HaDiff).
We prove the intermediate claim HaNotQ: a ∉ rational_numbers.
An exact proof term for the current goal is (setminusE2 R rational_numbers a HaDiff).
We prove the intermediate claim HUinLower: U ∈ R_lower_limit_topology.
We will prove U ∈ R_lower_limit_topology.
We will prove U ∈ generated_topology R R_lower_limit_basis.
We will prove U ∈ {U0 ∈ 𝒫 R|∀x0 ∈ U0, ∃b0 ∈ R_lower_limit_basis, x0 ∈ b0 ∧ b0 ⊆ U0}.
We prove the intermediate claim HUsub: U ⊆ R.
Let y be given.
Assume HyU.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z a)) y HyU).
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (PowerI R U HUsub).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b0 ∈ R_lower_limit_basis, x0 ∈ b0 ∧ b0 ⊆ U.
Let x0 be given.
Assume Hx0U.
We prove the intermediate claim Hx0R: x0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z a)) x0 Hx0U).
We prove the intermediate claim Hnx0a: ¬ (Rlt x0 a).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a)) x0 Hx0U).
Set b0 to be the term add_SNo x0 1.
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x0 Hx0R 1 real_1).
Set I0 to be the term halfopen_interval_left a b0.
We prove the intermediate claim HI0fam: I0 ∈ {halfopen_interval_left a bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a bb) b0 Hb0R).
We prove the intermediate claim HI0inB: I0 ∈ R_lower_limit_basis.
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a I0 HaR HI0fam).
We prove the intermediate claim Hx0InStd: x0 ∈ open_interval (add_SNo x0 (minus_SNo 1)) b0.
An exact proof term for the current goal is (real_in_open_interval_minus1_plus1 x0 Hx0R).
We prove the intermediate claim Hx0StdProp: Rlt (add_SNo x0 (minus_SNo 1)) x0 ∧ Rlt x0 b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt (add_SNo x0 (minus_SNo 1)) z ∧ Rlt z b0) x0 Hx0InStd).
We prove the intermediate claim Hx0b0: Rlt x0 b0.
An exact proof term for the current goal is (andER (Rlt (add_SNo x0 (minus_SNo 1)) x0) (Rlt x0 b0) Hx0StdProp).
We prove the intermediate claim Hx0InI0: x0 ∈ I0.
We prove the intermediate claim Hconj: ¬ (Rlt x0 a) ∧ Rlt x0 b0.
Apply andI to the current goal.
An exact proof term for the current goal is Hnx0a.
An exact proof term for the current goal is Hx0b0.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z b0) x0 Hx0R Hconj).
We prove the intermediate claim HI0subU: I0 ⊆ U.
Let y be given.
Assume HyI0.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z b0) y HyI0).
We prove the intermediate claim HyProp: ¬ (Rlt y a) ∧ Rlt y b0.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a) ∧ Rlt z b0) y HyI0).
We prove the intermediate claim Hnya: ¬ (Rlt y a).
An exact proof term for the current goal is (andEL (¬ (Rlt y a)) (Rlt y b0) HyProp).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a)) y HyR Hnya).
We use I0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HI0inB.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0InI0.
An exact proof term for the current goal is HI0subU.
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_lower_limit_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HUpow HUprop).
We prove the intermediate claim HUinRat: U ∈ generated_topology R rational_halfopen_intervals_basis.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HUinLower.
We prove the intermediate claim HUpropRat: ∀x0 ∈ U, ∃b0 ∈ rational_halfopen_intervals_basis, x0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ rational_halfopen_intervals_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HUinRat).
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a)) a HaR (not_Rlt_refl a HaR)).
Apply (HUpropRat a HaU) to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbInB: b ∈ rational_halfopen_intervals_basis.
Assume Hbrest: a ∈ b ∧ b ⊆ U.
We prove the intermediate claim Hab: a ∈ b.
An exact proof term for the current goal is (andEL (a ∈ b) (b ⊆ U) Hbrest).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (a ∈ b) (b ⊆ U) Hbrest).
We prove the intermediate claim Hexq1: ∃q1 ∈ rational_numbers, b ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}) b HbInB).
Apply Hexq1 to the current goal.
Let q1 be given.
Assume Hq1pair.
Apply Hq1pair to the current goal.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume HbFam: b ∈ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}.
We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, b = halfopen_interval_left q1 q2.
An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ halfopen_interval_left q1 q2) b HbFam).
Apply Hexq2 to the current goal.
Let q2 be given.
Assume Hq2pair.
Apply Hq2pair to the current goal.
Assume Hq2Q: q2 ∈ rational_numbers.
Assume HbEq: b = halfopen_interval_left q1 q2.
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 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 HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HaInInt: a ∈ halfopen_interval_left q1 q2.
rewrite the current goal using HbEq (from right to left).
An exact proof term for the current goal is Hab.
We prove the intermediate claim HaIntProp: ¬ (Rlt a q1) ∧ Rlt a q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) a HaInInt).
We prove the intermediate claim HnaRq1: ¬ (Rlt a q1).
An exact proof term for the current goal is (andEL (¬ (Rlt a q1)) (Rlt a q2) HaIntProp).
We prove the intermediate claim Haq2: Rlt a q2.
An exact proof term for the current goal is (andER (¬ (Rlt a q1)) (Rlt a q2) HaIntProp).
We prove the intermediate claim HnaLt: ¬ (a < q1).
Assume Haq1lt: a < q1.
We prove the intermediate claim Haq1: Rlt a q1.
An exact proof term for the current goal is (RltI a q1 HaR Hq1R Haq1lt).
An exact proof term for the current goal is (HnaRq1 Haq1).
We prove the intermediate claim Hq1lta: q1 < a.
Apply (SNoLt_trichotomy_or_impred a q1 HaS Hq1S (q1 < a)) to the current goal.
Assume Haq1lt: a < q1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnaLt Haq1lt).
Assume Haq1eq: a = q1.
We prove the intermediate claim HaQ: a ∈ rational_numbers.
rewrite the current goal using Haq1eq (from left to right).
An exact proof term for the current goal is Hq1Q.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HaNotQ HaQ).
Assume Hq1alt: q1 < a.
An exact proof term for the current goal is Hq1alt.
We prove the intermediate claim Hq1a: Rlt q1 a.
An exact proof term for the current goal is (RltI q1 a Hq1R HaR Hq1lta).
We prove the intermediate claim Haq2lt: a < q2.
An exact proof term for the current goal is (RltE_lt a q2 Haq2).
We prove the intermediate claim Hq1q2lt: q1 < q2.
An exact proof term for the current goal is (SNoLt_tra q1 a q2 Hq1S HaS Hq2S Hq1lta Haq2lt).
We prove the intermediate claim Hq1q2: Rlt q1 q2.
An exact proof term for the current goal is (RltI q1 q2 Hq1R Hq2R Hq1q2lt).
We prove the intermediate claim Hq1Inb: q1 ∈ b.
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (halfopen_interval_left_leftmem q1 q2 Hq1q2).
We prove the intermediate claim Hq1U: q1 ∈ U.
An exact proof term for the current goal is (HbsubU q1 Hq1Inb).
We prove the intermediate claim Hnq1a: ¬ (Rlt q1 a).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a)) q1 Hq1U).
An exact proof term for the current goal is (Hnq1a Hq1a).
∎