Let b be given.
Assume Hb.
Let x be given.
Assume Hxb.
We will prove ∃r ∈ rectangular_regions, x ∈ r ∧ r ⊆ b.
We prove the intermediate claim Hbprop: ∃c : set, ∃r0 : set, c ∈ EuclidPlane ∧ Rlt 0 r0 ∧ b = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
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}) b Hb).
Apply Hbprop to the current goal.
Let c be given.
Assume Hbprop2.
Apply Hbprop2 to the current goal.
Let r0 be given.
Assume Hbcore.
We prove the intermediate claim Hcr0: c ∈ EuclidPlane ∧ Rlt 0 r0.
An exact proof term for the current goal is (andEL (c ∈ EuclidPlane ∧ Rlt 0 r0) (b = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hbcore).
We prove the intermediate claim Hc: c ∈ EuclidPlane.
An exact proof term for the current goal is (andEL (c ∈ EuclidPlane) (Rlt 0 r0) Hcr0).
We prove the intermediate claim Hr0: Rlt 0 r0.
An exact proof term for the current goal is (andER (c ∈ EuclidPlane) (Rlt 0 r0) Hcr0).
We prove the intermediate claim HbEq: b = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
An exact proof term for the current goal is (andER (c ∈ EuclidPlane ∧ Rlt 0 r0) (b = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hbcore).
We prove the intermediate claim Hxb': x ∈ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
rewrite the current goal using HbEq (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HxE: x ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r0) x Hxb').
We prove the intermediate claim Hxball: Rlt (distance_R2 x c) r0.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r0) x Hxb').
Apply (rectangle_inside_ball x c r0 HxE Hc Hr0 Hxball) to the current goal.
Let r be given.
Assume Hrpair.
We use r to witness the existential quantifier.
We prove the intermediate claim Hr: r ∈ rectangular_regions.
An exact proof term for the current goal is (andEL (r ∈ rectangular_regions) (x ∈ r ∧ r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hrpair).
We prove the intermediate claim Hrprop: x ∈ r ∧ r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
An exact proof term for the current goal is (andER (r ∈ rectangular_regions) (x ∈ r ∧ r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hrpair).
We prove the intermediate claim Hxr: x ∈ r.
An exact proof term for the current goal is (andEL (x ∈ r) (r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hrprop).
We prove the intermediate claim Hrsub: r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
An exact proof term for the current goal is (andER (x ∈ r) (r ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}) Hrprop).
We prove the intermediate claim Hrsubb: r ⊆ b.
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is Hrsub.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
Apply andI to the current goal.
An exact proof term for the current goal is Hxr.
An exact proof term for the current goal is Hrsubb.
∎