We will prove basis_on EuclidPlane circular_regions.
We will prove circular_regions ⊆ 𝒫 EuclidPlane ∧ (∀x ∈ EuclidPlane, ∃b ∈ circular_regions, x ∈ b) ∧ (∀b1 ∈ circular_regions, ∀b2 ∈ circular_regions, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ circular_regions, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply and3I to the current goal.
Let U be given.
Assume HU: U ∈ circular_regions.
We will prove U ∈ 𝒫 EuclidPlane.
An exact proof term for the current goal is (SepE1 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃c : set, ∃r : set, c ∈ EuclidPlane ∧ Rlt 0 r ∧ U0 = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}) U HU).
We will prove ∀x ∈ EuclidPlane, ∃b ∈ circular_regions, x ∈ b.
Let x be given.
Assume Hx.
We use {p ∈ EuclidPlane|Rlt (distance_R2 p x) 1} to witness the existential quantifier.
Apply andI to the current goal.
We will prove {p ∈ EuclidPlane|Rlt (distance_R2 p x) 1} ∈ circular_regions.
An exact proof term for the current goal is (circular_regionI x 1 Hx Rlt_0_1).
We prove the intermediate claim Hlt: Rlt (distance_R2 x x) 1.
rewrite the current goal using (distance_R2_refl_0 x Hx) (from left to right).
We prove the intermediate claim HR: 0 ∈ R ∧ 1 ∈ R ∧ 0 < 1.
Apply and3I to the current goal.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is real_1.
An exact proof term for the current goal is SNoLt_0_1.
An exact proof term for the current goal is HR.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 x) 1) x Hx Hlt).
Let b1 be given.
Assume Hb1: b1 ∈ circular_regions.
Let b2 be given.
Assume Hb2: b2 ∈ circular_regions.
Let x be given.
Assume Hx1: x ∈ b1.
Assume Hx2: x ∈ b2.
We will prove ∃b3 ∈ circular_regions, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hb1prop: ∃c1 : set, ∃r1 : set, c1 ∈ EuclidPlane ∧ Rlt 0 r1 ∧ b1 = {p ∈ EuclidPlane|Rlt (distance_R2 p c1) r1}.
An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃c : set, ∃r : set, c ∈ EuclidPlane ∧ Rlt 0 r ∧ U0 = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}) b1 Hb1).
We prove the intermediate claim Hb2prop: ∃c2 : set, ∃r2 : set, c2 ∈ EuclidPlane ∧ Rlt 0 r2 ∧ b2 = {p ∈ EuclidPlane|Rlt (distance_R2 p c2) r2}.
An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃c : set, ∃r : set, c ∈ EuclidPlane ∧ Rlt 0 r ∧ U0 = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}) b2 Hb2).
Apply Hb1prop to the current goal.
Let c1 be given.
Assume Hb1prop2.
Apply Hb1prop2 to the current goal.
Let r1 be given.
Assume Hb1core.
Apply Hb2prop to the current goal.
Let c2 be given.
Assume Hb2prop2.
Apply Hb2prop2 to the current goal.
Let r2 be given.
Assume Hb2core.
We prove the intermediate claim Hc1r1: c1 ∈ EuclidPlane ∧ Rlt 0 r1.
An exact proof term for the current goal is (andEL (c1 ∈ EuclidPlane ∧ Rlt 0 r1) (b1 = {p ∈ EuclidPlane|Rlt (distance_R2 p c1) r1}) Hb1core).
We prove the intermediate claim Hc1: c1 ∈ EuclidPlane.
An exact proof term for the current goal is (andEL (c1 ∈ EuclidPlane) (Rlt 0 r1) Hc1r1).
We prove the intermediate claim Hr1: Rlt 0 r1.
An exact proof term for the current goal is (andER (c1 ∈ EuclidPlane) (Rlt 0 r1) Hc1r1).
We prove the intermediate claim Hb1eq: b1 = {p ∈ EuclidPlane|Rlt (distance_R2 p c1) r1}.
An exact proof term for the current goal is (andER (c1 ∈ EuclidPlane ∧ Rlt 0 r1) (b1 = {p ∈ EuclidPlane|Rlt (distance_R2 p c1) r1}) Hb1core).
We prove the intermediate claim Hc2r2: c2 ∈ EuclidPlane ∧ Rlt 0 r2.
An exact proof term for the current goal is (andEL (c2 ∈ EuclidPlane ∧ Rlt 0 r2) (b2 = {p ∈ EuclidPlane|Rlt (distance_R2 p c2) r2}) Hb2core).
We prove the intermediate claim Hc2: c2 ∈ EuclidPlane.
An exact proof term for the current goal is (andEL (c2 ∈ EuclidPlane) (Rlt 0 r2) Hc2r2).
We prove the intermediate claim Hr2: Rlt 0 r2.
An exact proof term for the current goal is (andER (c2 ∈ EuclidPlane) (Rlt 0 r2) Hc2r2).
We prove the intermediate claim Hb2eq: b2 = {p ∈ EuclidPlane|Rlt (distance_R2 p c2) r2}.
An exact proof term for the current goal is (andER (c2 ∈ EuclidPlane ∧ Rlt 0 r2) (b2 = {p ∈ EuclidPlane|Rlt (distance_R2 p c2) r2}) Hb2core).
We prove the intermediate claim Hx1': x ∈ {p ∈ EuclidPlane|Rlt (distance_R2 p c1) r1}.
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 Hx2': x ∈ {p ∈ EuclidPlane|Rlt (distance_R2 p c2) 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 HxEuclid: x ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c1) r1) x Hx1').
We prove the intermediate claim Hxball1: Rlt (distance_R2 x c1) r1.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c1) r1) x Hx1').
We prove the intermediate claim Hxball2: Rlt (distance_R2 x c2) r2.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c2) r2) x Hx2').
Apply (ball_refine_two_balls x c1 c2 r1 r2 HxEuclid Hc1 Hc2 Hr1 Hr2 Hxball1 Hxball2) to the current goal.
Let r3 be given.
Assume Hrefine2.
We prove the intermediate claim Hr3: Rlt 0 r3.
An exact proof term for the current goal is (andEL (Rlt 0 r3) (∀p : set, p ∈ EuclidPlane → Rlt (distance_R2 p x) r3 → Rlt (distance_R2 p c1) r1 ∧ Rlt (distance_R2 p c2) r2) Hrefine2).
We prove the intermediate claim HrefineP: ∀p : set, p ∈ EuclidPlane → Rlt (distance_R2 p x) r3 → Rlt (distance_R2 p c1) r1 ∧ Rlt (distance_R2 p c2) r2.
An exact proof term for the current goal is (andER (Rlt 0 r3) (∀p : set, p ∈ EuclidPlane → Rlt (distance_R2 p x) r3 → Rlt (distance_R2 p c1) r1 ∧ Rlt (distance_R2 p c2) r2) Hrefine2).
Set b3 to be the term {p ∈ EuclidPlane|Rlt (distance_R2 p x) r3}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We will prove b3 ∈ circular_regions.
We prove the intermediate claim Hb3def: b3 = {p ∈ EuclidPlane|Rlt (distance_R2 p x) r3}.
Use reflexivity.
rewrite the current goal using Hb3def (from left to right).
An exact proof term for the current goal is (circular_regionI x r3 HxEuclid Hr3).
Apply andI to the current goal.
We will prove x ∈ b3.
We prove the intermediate claim Hdx: Rlt (distance_R2 x x) r3.
rewrite the current goal using (distance_R2_refl_0 x HxEuclid) (from left to right).
An exact proof term for the current goal is Hr3.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 x) r3) x HxEuclid Hdx).
We will prove b3 ⊆ b1 ∩ b2.
Let p be given.
Assume Hp3: p ∈ b3.
We will prove p ∈ b1 ∩ b2.
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 x) r3) p Hp3).
We prove the intermediate claim Hpball: Rlt (distance_R2 p x) r3.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 x) r3) p Hp3).
We prove the intermediate claim Hboth: Rlt (distance_R2 p c1) r1 ∧ Rlt (distance_R2 p c2) r2.
An exact proof term for the current goal is (HrefineP p HpE Hpball).
We prove the intermediate claim Hpball1: Rlt (distance_R2 p c1) r1.
An exact proof term for the current goal is (andEL (Rlt (distance_R2 p c1) r1) (Rlt (distance_R2 p c2) r2) Hboth).
We prove the intermediate claim Hpball2: Rlt (distance_R2 p c2) r2.
An exact proof term for the current goal is (andER (Rlt (distance_R2 p c1) r1) (Rlt (distance_R2 p c2) r2) Hboth).
We prove the intermediate claim Hpb1: p ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c1) r1) p HpE Hpball1).
We prove the intermediate claim Hpb2: p ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c2) r2) p HpE Hpball2).
An exact proof term for the current goal is (binintersectI b1 b2 p Hpb1 Hpb2).
∎