Let b be given.

Assume Hb.

Let x be given.

Assume Hxb.

We will prove ∃u ∈ circular_regions, x ∈ u ∧ u ⊆ b.

We prove the intermediate claim Hbprop: ∃a : set, ∃b0 : set, ∃c : set, ∃d0 : set, a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0 ∧ b = {p ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0}.

An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃a b c d : set, a ∈ R ∧ b ∈ R ∧ c ∈ R ∧ d ∈ R ∧ Rlt a b ∧ Rlt c d ∧ U0 = {p1 ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p1 = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b ∧ Rlt c y0 ∧ Rlt y0 d}) b Hb).

Apply Hbprop to the current goal.

Let a be given.

Assume Hbprop2.

Apply Hbprop2 to the current goal.

Let b0 be given.

Assume Hbprop3.

Apply Hbprop3 to the current goal.

Let c be given.

Assume Hbprop4.

Apply Hbprop4 to the current goal.

Let d0 be given.

Assume Hbcore.

We prove the intermediate claim HbEq: b = {p ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0}.

An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0) (b = {p ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0}) Hbcore).

We prove the intermediate claim Hxb': x ∈ {p ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0}.

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 (λp1 : set ⇒ ∃x0 : set, ∃y0 : set, p1 = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0) x Hxb').

Apply (ball_inside_rectangle b x Hb HxE Hxb) to the current goal.

Let r3 be given.

Assume Hrad2.

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 → p ∈ b) Hrad2).

We prove the intermediate claim HradP: ∀p : set, p ∈ EuclidPlane → Rlt (distance_R2 p x) r3 → p ∈ b.

An exact proof term for the current goal is (andER (Rlt 0 r3) (∀p : set, p ∈ EuclidPlane → Rlt (distance_R2 p x) r3 → p ∈ b) Hrad2).

Set u to be the term {p ∈ EuclidPlane|Rlt (distance_R2 p x) r3}.

We use u to witness the existential quantifier.

Apply andI to the current goal.

We will prove u ∈ circular_regions.

We prove the intermediate claim HuDef: u = {p ∈ EuclidPlane|Rlt (distance_R2 p x) r3}.

Use reflexivity.

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

An exact proof term for the current goal is (circular_regionI x r3 HxE Hr3).

Apply andI to the current goal.

We will prove x ∈ u.

We prove the intermediate claim HxBall: Rlt (distance_R2 x x) r3.

rewrite the current goal using (distance_R2_refl_0 x HxE) (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 HxE HxBall).

We will prove u ⊆ b.

Let p be given.

Assume Hp: p ∈ u.

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

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

An exact proof term for the current goal is (HradP p HpE HpBall).

∎