Let x be given.
Assume Hx: x ∈ ex17_17_interval_A_closure_C.
We will prove x ∈ closure_of R R_C_topology ex17_17_interval_A.
Set A to be the term ex17_17_interval_A.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ 0 ≤ z ∧ z ≤ sqrt2) x Hx).
We prove the intermediate claim HxProp: 0 ≤ x ∧ x ≤ sqrt2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ 0 ≤ z ∧ z ≤ sqrt2) x Hx).
We prove the intermediate claim H0lex: 0 ≤ x.
An exact proof term for the current goal is (andEL (0 ≤ x) (x ≤ sqrt2) HxProp).
We prove the intermediate claim HxleS2: x ≤ sqrt2.
An exact proof term for the current goal is (andER (0 ≤ x) (x ≤ sqrt2) HxProp).
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 Hs2R: sqrt2 ∈ R.
An exact proof term for the current goal is sqrt2_in_R.
We prove the intermediate claim Hs2S: SNo sqrt2.
An exact proof term for the current goal is (real_SNo sqrt2 Hs2R).
We prove the intermediate claim Hcl: ∀U : set, U ∈ R_C_topology → x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ R_C_topology.
Assume HxU: x ∈ U.
We will prove U ∩ A ≠ Empty.
We prove the intermediate claim Hcases0: 0 < x ∨ 0 = x.
An exact proof term for the current goal is (SNoLeE 0 x SNo_0 HxS H0lex).
Apply Hcases0 to the current goal.
Assume H0ltx: 0 < x.
We prove the intermediate claim HcasesS2: x < sqrt2 ∨ x = sqrt2.
An exact proof term for the current goal is (SNoLeE x sqrt2 HxS Hs2S HxleS2).
Apply HcasesS2 to the current goal.
Assume HxltS2: x < sqrt2.
We prove the intermediate claim H0ltxR: Rlt 0 x.
An exact proof term for the current goal is (RltI 0 x real_0 HxR H0ltx).
We prove the intermediate claim HxltS2R: Rlt x sqrt2.
An exact proof term for the current goal is (RltI x sqrt2 HxR Hs2R HxltS2).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) x HxR (andI (Rlt 0 x) (Rlt x sqrt2) H0ltxR HxltS2R)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxUA: x ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A x HxU HxA).
We prove the intermediate claim HxEmp: x ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HxUA.
An exact proof term for the current goal is (EmptyE x HxEmp).
Assume HxeqS2: x = sqrt2.
Set s2 to be the term sqrt2.
We prove the intermediate claim Hs2U: s2 ∈ U.
rewrite the current goal using HxeqS2 (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hneigh: ∀z ∈ U, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ rational_halfopen_intervals_basis, s2 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Hneigh s2 Hs2U).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbB: b ∈ rational_halfopen_intervals_basis.
Assume Hbcore: s2 ∈ b ∧ b ⊆ U.
We prove the intermediate claim Hs2b: s2 ∈ b.
An exact proof term for the current goal is (andEL (s2 ∈ b) (b ⊆ U) Hbcore).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (s2 ∈ b) (b ⊆ U) Hbcore).
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 HbB).
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 Hs2Inb: s2 ∈ halfopen_interval_left q1 q2.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hs2b.
We prove the intermediate claim Hs2bprop: ¬ (Rlt s2 q1) ∧ Rlt s2 q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) s2 Hs2Inb).
We prove the intermediate claim Hnots2q1: ¬ (Rlt s2 q1).
An exact proof term for the current goal is (andEL (¬ (Rlt s2 q1)) (Rlt s2 q2) Hs2bprop).
We prove the intermediate claim Hs2ltq2: Rlt s2 q2.
An exact proof term for the current goal is (andER (¬ (Rlt s2 q1)) (Rlt s2 q2) Hs2bprop).
We prove the intermediate claim H0ltS2R: Rlt 0 s2.
An exact proof term for the current goal is (RltI 0 s2 real_0 Hs2R SNoLt_0_sqrt2).
We prove the intermediate claim Hq1ltS2R: Rlt q1 s2.
Apply (SNoLt_trichotomy_or_impred q1 s2 Hq1S Hs2S (Rlt q1 s2)) to the current goal.
Assume Hlt: q1 < s2.
An exact proof term for the current goal is (RltI q1 s2 Hq1R Hs2R Hlt).
Assume Heq: q1 = s2.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2Q: s2 ∈ rational_numbers.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hq1Q.
An exact proof term for the current goal is (sqrt2_not_rational_numbers Hs2Q).
Assume Hgt: s2 < q1.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2ltq1: Rlt s2 q1.
An exact proof term for the current goal is (RltI s2 q1 Hs2R Hq1R Hgt).
An exact proof term for the current goal is (Hnots2q1 Hs2ltq1).
We prove the intermediate claim Hq1ltS2: q1 < s2.
An exact proof term for the current goal is (RltE_lt q1 s2 Hq1ltS2R).
Apply (SNoLt_trichotomy_or_impred q1 0 Hq1S SNo_0 (U ∩ A ≠ Empty)) to the current goal.
Assume Hq1lt0: q1 < 0.
We prove the intermediate claim Hq1lt0R: Rlt q1 0.
An exact proof term for the current goal is (RltI q1 0 Hq1R real_0 Hq1lt0).
Apply (rational_dense_between_reals 0 s2 real_0 Hs2R H0ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q s2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q s2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q s2 q2 HqltS2 Hs2ltq2).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
Assume Hqq1: Rlt q q1.
We prove the intermediate claim Hq0: Rlt q 0.
An exact proof term for the current goal is (Rlt_tra q q1 0 Hqq1 Hq1lt0R).
An exact proof term for the current goal is ((not_Rlt_sym 0 q H0ltq) Hq0).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z s2) q HqR (andI (Rlt 0 q) (Rlt q s2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume Hq1eq0: q1 = 0.
Apply (rational_dense_between_reals 0 s2 real_0 Hs2R H0ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q s2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q s2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q s2 q2 HqltS2 Hs2ltq2).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
rewrite the current goal using Hq1eq0 (from left to right).
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z s2) q HqR (andI (Rlt 0 q) (Rlt q s2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume H0ltq1: 0 < q1.
Apply (rational_dense_between_reals q1 s2 Hq1R Hs2R Hq1ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt q1 q ∧ Rlt q s2.
We prove the intermediate claim Hq1ltq: Rlt q1 q.
An exact proof term for the current goal is (andEL (Rlt q1 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q s2.
An exact proof term for the current goal is (andER (Rlt q1 q) (Rlt q s2) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 q1 q (RltI 0 q1 real_0 Hq1R H0ltq1) Hq1ltq).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q s2 q2 HqltS2 Hs2ltq2).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
An exact proof term for the current goal is (not_Rlt_sym q1 q Hq1ltq).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z s2) q HqR (andI (Rlt 0 q) (Rlt q s2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume H0eqx: 0 = x.
We prove the intermediate claim H0U: 0 ∈ U.
rewrite the current goal using H0eqx (from left to right).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hneigh: ∀z ∈ U, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ rational_halfopen_intervals_basis, z ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ rational_halfopen_intervals_basis, 0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Hneigh 0 H0U).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbB: b ∈ rational_halfopen_intervals_basis.
Assume Hbcore: 0 ∈ b ∧ b ⊆ U.
We prove the intermediate claim H0b: 0 ∈ b.
An exact proof term for the current goal is (andEL (0 ∈ b) (b ⊆ U) Hbcore).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (0 ∈ b) (b ⊆ U) Hbcore).
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 HbB).
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 H0Inb: 0 ∈ halfopen_interval_left q1 q2.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is H0b.
We prove the intermediate claim H0bprop: ¬ (Rlt 0 q1) ∧ Rlt 0 q2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) 0 H0Inb).
We prove the intermediate claim H0ltq2: Rlt 0 q2.
An exact proof term for the current goal is (andER (¬ (Rlt 0 q1)) (Rlt 0 q2) H0bprop).
We prove the intermediate claim H0ltS2R: Rlt 0 sqrt2.
An exact proof term for the current goal is (RltI 0 sqrt2 real_0 Hs2R SNoLt_0_sqrt2).
Apply (SNoLt_trichotomy_or_impred q2 sqrt2 (real_SNo q2 Hq2R) Hs2S (U ∩ A ≠ Empty)) to the current goal.
Assume Hq2ltS2: q2 < sqrt2.
We prove the intermediate claim Hq2ltS2R: Rlt q2 sqrt2.
An exact proof term for the current goal is (RltI q2 sqrt2 Hq2R Hs2R Hq2ltS2).
Apply (rational_dense_between_reals 0 q2 real_0 Hq2R H0ltq2) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q q2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q q2) Hqprop).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q q2) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqltS2: Rlt q sqrt2.
An exact proof term for the current goal is (Rlt_tra q q2 sqrt2 Hqltq2 Hq2ltS2R).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
Assume Hqq1: Rlt q q1.
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (Rlt_tra 0 q q1 H0ltq Hqq1).
An exact proof term for the current goal is ((andEL (¬ (Rlt 0 q1)) (Rlt 0 q2) H0bprop) H0ltq1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR (andI (Rlt 0 q) (Rlt q sqrt2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume Hq2eqS2: q2 = sqrt2.
Apply (rational_dense_between_reals 0 sqrt2 real_0 Hs2R H0ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q sqrt2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q sqrt2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q sqrt2) Hqprop).
We prove the intermediate claim Hqltq2: Rlt q q2.
rewrite the current goal using Hq2eqS2 (from left to right).
An exact proof term for the current goal is HqltS2.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
Assume Hqq1: Rlt q q1.
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (Rlt_tra 0 q q1 H0ltq Hqq1).
An exact proof term for the current goal is ((andEL (¬ (Rlt 0 q1)) (Rlt 0 q2) H0bprop) H0ltq1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR (andI (Rlt 0 q) (Rlt q sqrt2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
Assume Hs2ltq2: sqrt2 < q2.
Apply (rational_dense_between_reals 0 sqrt2 real_0 Hs2R H0ltS2R) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q sqrt2.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q sqrt2) Hqprop).
We prove the intermediate claim HqltS2: Rlt q sqrt2.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q sqrt2) Hqprop).
We prove the intermediate claim Hs2ltq2R: Rlt sqrt2 q2.
An exact proof term for the current goal is (RltI sqrt2 q2 Hs2R Hq2R Hs2ltq2).
We prove the intermediate claim Hqltq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q sqrt2 q2 HqltS2 Hs2ltq2R).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hnotqq1: ¬ (Rlt q q1).
Assume Hqq1: Rlt q q1.
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (Rlt_tra 0 q q1 H0ltq Hqq1).
An exact proof term for the current goal is ((andEL (¬ (Rlt 0 q1)) (Rlt 0 q2) H0bprop) H0ltq1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z q1) ∧ Rlt z q2) q HqR (andI (¬ (Rlt q q1)) (Rlt q q2) Hnotqq1 Hqltq2)).
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbsubU q HqInb).
We prove the intermediate claim HqInA: q ∈ A.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z sqrt2) q HqR (andI (Rlt 0 q) (Rlt q sqrt2) H0ltq HqltS2)).
Assume Hemp: U ∩ A = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HqUA: q ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A q HqInU HqInA).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using Hemp (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ∀U : set, U ∈ R_C_topology → x0 ∈ U → U ∩ A ≠ Empty) x HxR Hcl).
∎