Let b1 be given.

Let b2 be given.

Let p be given.

Assume Hp1: p ∈ b1.

Assume Hp2: p ∈ b2.

We will prove ∃b3 ∈ rectangular_regions, p ∈ b3 ∧ b3 ⊆ b1 ∩ b2.

We prove the intermediate claim Hb1prop: ∃a1 : set, ∃b1x : set, ∃c1 : set, ∃d1 : set, a1 ∈ R ∧ b1x ∈ R ∧ c1 ∈ R ∧ d1 ∈ R ∧ Rlt a1 b1x ∧ Rlt c1 d1 ∧ b1 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1}.

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}) b1 Hb1).

Apply Hb1prop to the current goal.

Let a1 be given.

Assume Hb1prop2.

Apply Hb1prop2 to the current goal.

Let b1x be given.

Assume Hb1prop3.

Apply Hb1prop3 to the current goal.

Let c1 be given.

Assume Hb1prop4.

Apply Hb1prop4 to the current goal.

Let d1 be given.

Assume Hb1core.

We prove the intermediate claim Hb2prop: ∃a2 : set, ∃b2x : set, ∃c2 : set, ∃d2 : set, a2 ∈ R ∧ b2x ∈ R ∧ c2 ∈ R ∧ d2 ∈ R ∧ Rlt a2 b2x ∧ Rlt c2 d2 ∧ b2 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2}.

Apply Hb2prop to the current goal.

Let a2 be given.

Assume Hb2prop2.

Apply Hb2prop2 to the current goal.

Let b2x be given.

Assume Hb2prop3.

Apply Hb2prop3 to the current goal.

Let c2 be given.

Assume Hb2prop4.

Apply Hb2prop4 to the current goal.

Let d2 be given.

Assume Hb2core.

We prove the intermediate claim Hb1eq: b1 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1}.

An exact proof term for the current goal is (andER (a1 ∈ R ∧ b1x ∈ R ∧ c1 ∈ R ∧ d1 ∈ R ∧ Rlt a1 b1x ∧ Rlt c1 d1) (b1 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1}) Hb1core).

We prove the intermediate claim Hb2eq: b2 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2}.

An exact proof term for the current goal is (andER (a2 ∈ R ∧ b2x ∈ R ∧ c2 ∈ R ∧ d2 ∈ R ∧ Rlt a2 b2x ∧ Rlt c2 d2) (b2 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2}) Hb2core).

We prove the intermediate claim Hp1': p ∈ {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1}.

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

An exact proof term for the current goal is Hp1.

We prove the intermediate claim Hp2': p ∈ {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2}.

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

An exact proof term for the current goal is Hp2.

We prove the intermediate claim Hp1coords: ∃x1 : set, ∃y1 : set, p = (x1,y1) ∧ Rlt a1 x1 ∧ Rlt x1 b1x ∧ Rlt c1 y1 ∧ Rlt y1 d1.

An exact proof term for the current goal is (SepE2 EuclidPlane (λq : set ⇒ ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1) p Hp1').

We prove the intermediate claim Hp2coords: ∃x2 : set, ∃y2 : set, p = (x2,y2) ∧ Rlt a2 x2 ∧ Rlt x2 b2x ∧ Rlt c2 y2 ∧ Rlt y2 d2.

An exact proof term for the current goal is (SepE2 EuclidPlane (λq : set ⇒ ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2) p Hp2').

Apply Hp1coords to the current goal.

Let x1 be given.

Assume Hp1coords2.

Apply Hp1coords2 to the current goal.

Let y1 be given.

Assume Hp1ineq.

Apply Hp2coords to the current goal.

Let x2 be given.

Assume Hp2coords2.

Apply Hp2coords2 to the current goal.

Let y2 be given.

Assume Hp2ineq.

We prove the intermediate claim Hp_tup1: p = (x1,y1).

We prove the intermediate claim H1: (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1).

An exact proof term for the current goal is (andEL (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1) (Rlt y1 d1) Hp1ineq).

We prove the intermediate claim H2: ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x).

An exact proof term for the current goal is (andEL ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) (Rlt c1 y1) H1).

We prove the intermediate claim H3: (p = (x1,y1) ∧ Rlt a1 x1).

An exact proof term for the current goal is (andEL (p = (x1,y1) ∧ Rlt a1 x1) (Rlt x1 b1x) H2).

An exact proof term for the current goal is (andEL (p = (x1,y1)) (Rlt a1 x1) H3).

We prove the intermediate claim Hp_tup2: p = (x2,y2).

We prove the intermediate claim H1: (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2).

An exact proof term for the current goal is (andEL (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2) (Rlt y2 d2) Hp2ineq).

We prove the intermediate claim H2: ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x).

An exact proof term for the current goal is (andEL ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) (Rlt c2 y2) H1).

We prove the intermediate claim H3: (p = (x2,y2) ∧ Rlt a2 x2).

An exact proof term for the current goal is (andEL (p = (x2,y2) ∧ Rlt a2 x2) (Rlt x2 b2x) H2).

An exact proof term for the current goal is (andEL (p = (x2,y2)) (Rlt a2 x2) H3).

We prove the intermediate claim Heq12: (x1,y1) = (x2,y2).

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

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

Use reflexivity.

We prove the intermediate claim Hcoords: x1 = x2 ∧ y1 = y2.

An exact proof term for the current goal is (tuple_eq_coords_R2 x1 y1 x2 y2 Heq12).

We prove the intermediate claim Hx1eq: x1 = x2.

An exact proof term for the current goal is (andEL (x1 = x2) (y1 = y2) Hcoords).

We prove the intermediate claim Hy1eq: y1 = y2.

An exact proof term for the current goal is (andER (x1 = x2) (y1 = y2) Hcoords).

We prove the intermediate claim Ha1x1: Rlt a1 x1.

We prove the intermediate claim H1: (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1).

An exact proof term for the current goal is (andEL (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1) (Rlt y1 d1) Hp1ineq).

We prove the intermediate claim H2: ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x).

An exact proof term for the current goal is (andEL ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) (Rlt c1 y1) H1).

We prove the intermediate claim H3: (p = (x1,y1) ∧ Rlt a1 x1).

An exact proof term for the current goal is (andEL (p = (x1,y1) ∧ Rlt a1 x1) (Rlt x1 b1x) H2).

An exact proof term for the current goal is (andER (p = (x1,y1)) (Rlt a1 x1) H3).

We prove the intermediate claim Hx1b1: Rlt x1 b1x.

We prove the intermediate claim H1: (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1).

An exact proof term for the current goal is (andEL (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1) (Rlt y1 d1) Hp1ineq).

We prove the intermediate claim H2: ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x).

An exact proof term for the current goal is (andEL ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) (Rlt c1 y1) H1).

An exact proof term for the current goal is (andER (p = (x1,y1) ∧ Rlt a1 x1) (Rlt x1 b1x) H2).

We prove the intermediate claim Hc1y1: Rlt c1 y1.

We prove the intermediate claim H1: (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1).

An exact proof term for the current goal is (andEL (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1) (Rlt y1 d1) Hp1ineq).

An exact proof term for the current goal is (andER ((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) (Rlt c1 y1) H1).

We prove the intermediate claim Hy1d1: Rlt y1 d1.

An exact proof term for the current goal is (andER (((p = (x1,y1) ∧ Rlt a1 x1) ∧ Rlt x1 b1x) ∧ Rlt c1 y1) (Rlt y1 d1) Hp1ineq).

We prove the intermediate claim Ha2x2: Rlt a2 x2.

We prove the intermediate claim H1: (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2).

An exact proof term for the current goal is (andEL (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2) (Rlt y2 d2) Hp2ineq).

We prove the intermediate claim H2: ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x).

An exact proof term for the current goal is (andEL ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) (Rlt c2 y2) H1).

We prove the intermediate claim H3: (p = (x2,y2) ∧ Rlt a2 x2).

An exact proof term for the current goal is (andEL (p = (x2,y2) ∧ Rlt a2 x2) (Rlt x2 b2x) H2).

An exact proof term for the current goal is (andER (p = (x2,y2)) (Rlt a2 x2) H3).

We prove the intermediate claim Hx2b2: Rlt x2 b2x.

We prove the intermediate claim H1: (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2).

An exact proof term for the current goal is (andEL (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2) (Rlt y2 d2) Hp2ineq).

We prove the intermediate claim H2: ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x).

An exact proof term for the current goal is (andEL ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) (Rlt c2 y2) H1).

An exact proof term for the current goal is (andER (p = (x2,y2) ∧ Rlt a2 x2) (Rlt x2 b2x) H2).

We prove the intermediate claim Hc2y2: Rlt c2 y2.

We prove the intermediate claim H1: (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2).

An exact proof term for the current goal is (andEL (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2) (Rlt y2 d2) Hp2ineq).

An exact proof term for the current goal is (andER ((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) (Rlt c2 y2) H1).

We prove the intermediate claim Hy2d2: Rlt y2 d2.

An exact proof term for the current goal is (andER (((p = (x2,y2) ∧ Rlt a2 x2) ∧ Rlt x2 b2x) ∧ Rlt c2 y2) (Rlt y2 d2) Hp2ineq).

We prove the intermediate claim Ha2x1: Rlt a2 x1.

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

An exact proof term for the current goal is Ha2x2.

We prove the intermediate claim Hx1b2: Rlt x1 b2x.

rewrite the current goal using Hx1eq (from left to right) at position 1.

An exact proof term for the current goal is Hx2b2.

We prove the intermediate claim Hc2y1: Rlt c2 y1.

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

An exact proof term for the current goal is Hc2y2.

We prove the intermediate claim Hy1d2: Rlt y1 d2.

rewrite the current goal using Hy1eq (from left to right) at position 1.

An exact proof term for the current goal is Hy2d2.

Set a3 to be the term if a1 < a2 then a2 else a1.

Set b3x to be the term if b1x < b2x then b1x else b2x.

Set c3 to be the term if c1 < c2 then c2 else c1.

Set d3 to be the term if d1 < d2 then d1 else d2.

We prove the intermediate claim Ha3def: a3 = if a1 < a2 then a2 else a1.

Use reflexivity.

We prove the intermediate claim Hb3def: b3x = if b1x < b2x then b1x else b2x.

Use reflexivity.

We prove the intermediate claim Hc3def: c3 = if c1 < c2 then c2 else c1.

Use reflexivity.

We prove the intermediate claim Hd3def: d3 = if d1 < d2 then d1 else d2.

Use reflexivity.

We prove the intermediate claim Hb1params: a1 ∈ R ∧ b1x ∈ R ∧ c1 ∈ R ∧ d1 ∈ R ∧ Rlt a1 b1x ∧ Rlt c1 d1.

An exact proof term for the current goal is (andEL (a1 ∈ R ∧ b1x ∈ R ∧ c1 ∈ R ∧ d1 ∈ R ∧ Rlt a1 b1x ∧ Rlt c1 d1) (b1 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1}) Hb1core).

We prove the intermediate claim Hb2params: a2 ∈ R ∧ b2x ∈ R ∧ c2 ∈ R ∧ d2 ∈ R ∧ Rlt a2 b2x ∧ Rlt c2 d2.

An exact proof term for the current goal is (andEL (a2 ∈ R ∧ b2x ∈ R ∧ c2 ∈ R ∧ d2 ∈ R ∧ Rlt a2 b2x ∧ Rlt c2 d2) (b2 = {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2}) Hb2core).

We prove the intermediate claim Hb1left: ((((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) ∧ d1 ∈ R) ∧ Rlt a1 b1x).

An exact proof term for the current goal is (andEL ((((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) ∧ d1 ∈ R) ∧ Rlt a1 b1x) (Rlt c1 d1) Hb1params).

We prove the intermediate claim Hb2left: ((((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) ∧ d2 ∈ R) ∧ Rlt a2 b2x).

An exact proof term for the current goal is (andEL ((((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) ∧ d2 ∈ R) ∧ Rlt a2 b2x) (Rlt c2 d2) Hb2params).

We prove the intermediate claim Ha1b1x_c1_d1: (((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) ∧ d1 ∈ R).

An exact proof term for the current goal is (andEL (((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) ∧ d1 ∈ R) (Rlt a1 b1x) Hb1left).

We prove the intermediate claim Ha2b2x_c2_d2: (((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) ∧ d2 ∈ R).

An exact proof term for the current goal is (andEL (((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) ∧ d2 ∈ R) (Rlt a2 b2x) Hb2left).

We prove the intermediate claim Ha1b1x_c1: ((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R).

An exact proof term for the current goal is (andEL ((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) (d1 ∈ R) Ha1b1x_c1_d1).

We prove the intermediate claim Ha2b2x_c2: ((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R).

An exact proof term for the current goal is (andEL ((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) (d2 ∈ R) Ha2b2x_c2_d2).

We prove the intermediate claim Ha1b1x: a1 ∈ R ∧ b1x ∈ R.

An exact proof term for the current goal is (andEL (a1 ∈ R ∧ b1x ∈ R) (c1 ∈ R) Ha1b1x_c1).

We prove the intermediate claim Ha2b2x: a2 ∈ R ∧ b2x ∈ R.

An exact proof term for the current goal is (andEL (a2 ∈ R ∧ b2x ∈ R) (c2 ∈ R) Ha2b2x_c2).

We prove the intermediate claim Ha1R: a1 ∈ R.

An exact proof term for the current goal is (andEL (a1 ∈ R) (b1x ∈ R) Ha1b1x).

We prove the intermediate claim Hb1xR: b1x ∈ R.

An exact proof term for the current goal is (andER (a1 ∈ R) (b1x ∈ R) Ha1b1x).

We prove the intermediate claim Hc1R: c1 ∈ R.

An exact proof term for the current goal is (andER (a1 ∈ R ∧ b1x ∈ R) (c1 ∈ R) Ha1b1x_c1).

We prove the intermediate claim Hd1R: d1 ∈ R.

An exact proof term for the current goal is (andER ((a1 ∈ R ∧ b1x ∈ R) ∧ c1 ∈ R) (d1 ∈ R) Ha1b1x_c1_d1).

We prove the intermediate claim Ha2R: a2 ∈ R.

An exact proof term for the current goal is (andEL (a2 ∈ R) (b2x ∈ R) Ha2b2x).

We prove the intermediate claim Hb2xR: b2x ∈ R.

An exact proof term for the current goal is (andER (a2 ∈ R) (b2x ∈ R) Ha2b2x).

We prove the intermediate claim Hc2R: c2 ∈ R.

An exact proof term for the current goal is (andER (a2 ∈ R ∧ b2x ∈ R) (c2 ∈ R) Ha2b2x_c2).

We prove the intermediate claim Hd2R: d2 ∈ R.

An exact proof term for the current goal is (andER ((a2 ∈ R ∧ b2x ∈ R) ∧ c2 ∈ R) (d2 ∈ R) Ha2b2x_c2_d2).

We prove the intermediate claim Ha3R: a3 ∈ R.

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

Apply (xm (a1 < a2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (a1 < a2) a2 a1 Hlt) (from left to right).

An exact proof term for the current goal is Ha2R.

Assume Hnlt.

rewrite the current goal using (If_i_0 (a1 < a2) a2 a1 Hnlt) (from left to right).

An exact proof term for the current goal is Ha1R.

We prove the intermediate claim Hb3xR: b3x ∈ R.

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

Apply (xm (b1x < b2x)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (b1x < b2x) b1x b2x Hlt) (from left to right).

An exact proof term for the current goal is Hb1xR.

Assume Hnlt.

rewrite the current goal using (If_i_0 (b1x < b2x) b1x b2x Hnlt) (from left to right).

An exact proof term for the current goal is Hb2xR.

We prove the intermediate claim Hc3R: c3 ∈ R.

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

Apply (xm (c1 < c2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (c1 < c2) c2 c1 Hlt) (from left to right).

An exact proof term for the current goal is Hc2R.

Assume Hnlt.

rewrite the current goal using (If_i_0 (c1 < c2) c2 c1 Hnlt) (from left to right).

An exact proof term for the current goal is Hc1R.

We prove the intermediate claim Hd3R: d3 ∈ R.

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

Apply (xm (d1 < d2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (d1 < d2) d1 d2 Hlt) (from left to right).

An exact proof term for the current goal is Hd1R.

Assume Hnlt.

rewrite the current goal using (If_i_0 (d1 < d2) d1 d2 Hnlt) (from left to right).

An exact proof term for the current goal is Hd2R.

We prove the intermediate claim Hax3: Rlt a3 x1.

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

Apply (xm (a1 < a2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (a1 < a2) a2 a1 Hlt) (from left to right).

An exact proof term for the current goal is Ha2x1.

Assume Hnlt.

rewrite the current goal using (If_i_0 (a1 < a2) a2 a1 Hnlt) (from left to right).

An exact proof term for the current goal is Ha1x1.

We prove the intermediate claim Hxb3: Rlt x1 b3x.

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

Apply (xm (b1x < b2x)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (b1x < b2x) b1x b2x Hlt) (from left to right).

An exact proof term for the current goal is Hx1b1.

Assume Hnlt.

rewrite the current goal using (If_i_0 (b1x < b2x) b1x b2x Hnlt) (from left to right).

An exact proof term for the current goal is Hx1b2.

We prove the intermediate claim Hcy3: Rlt c3 y1.

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

Apply (xm (c1 < c2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (c1 < c2) c2 c1 Hlt) (from left to right).

An exact proof term for the current goal is Hc2y1.

Assume Hnlt.

rewrite the current goal using (If_i_0 (c1 < c2) c2 c1 Hnlt) (from left to right).

An exact proof term for the current goal is Hc1y1.

We prove the intermediate claim Hyd3: Rlt y1 d3.

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

Apply (xm (d1 < d2)) to the current goal.

Assume Hlt.

rewrite the current goal using (If_i_1 (d1 < d2) d1 d2 Hlt) (from left to right).

An exact proof term for the current goal is Hy1d1.

Assume Hnlt.

rewrite the current goal using (If_i_0 (d1 < d2) d1 d2 Hnlt) (from left to right).

An exact proof term for the current goal is Hy1d2.

Set b3rect to be the term {q ∈ EuclidPlane|∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3}.

We use b3rect to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim Hb3pow: b3rect ∈ 𝒫 EuclidPlane.

Apply PowerI EuclidPlane b3rect to the current goal.

Let q be given.

Assume Hq: q ∈ b3rect.

An exact proof term for the current goal is (SepE1 EuclidPlane (λq0 : set ⇒ ∃x0 : set, ∃y0 : set, q0 = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3) q Hq).

We prove the intermediate claim Hab3: Rlt a3 b3x.

An exact proof term for the current goal is (Rlt_tra a3 x1 b3x Hax3 Hxb3).

We prove the intermediate claim Hcd3: Rlt c3 d3.

An exact proof term for the current goal is (Rlt_tra c3 y1 d3 Hcy3 Hyd3).

We prove the intermediate claim Hprop: ∃a0 : set, ∃b0 : set, ∃c0 : set, ∃d0 : set, a0 ∈ R ∧ b0 ∈ R ∧ c0 ∈ R ∧ d0 ∈ R ∧ Rlt a0 b0 ∧ Rlt c0 d0 ∧ b3rect = {p1 ∈ EuclidPlane|∃x0 : set, ∃y0 : set, p1 = (x0,y0) ∧ Rlt a0 x0 ∧ Rlt x0 b0 ∧ Rlt c0 y0 ∧ Rlt y0 d0}.

We use a3 to witness the existential quantifier.

We use b3x to witness the existential quantifier.

We use c3 to witness the existential quantifier.

We use d3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim H12345: a3 ∈ R ∧ b3x ∈ R ∧ c3 ∈ R ∧ d3 ∈ R ∧ Rlt a3 b3x ∧ Rlt c3 d3.

Apply and6I to the current goal.

An exact proof term for the current goal is Ha3R.

An exact proof term for the current goal is Hb3xR.

An exact proof term for the current goal is Hc3R.

An exact proof term for the current goal is Hd3R.

An exact proof term for the current goal is Hab3.

An exact proof term for the current goal is Hcd3.

An exact proof term for the current goal is H12345.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 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}) b3rect Hb3pow Hprop).

Apply andI to the current goal.

We prove the intermediate claim HpEuclid: p ∈ EuclidPlane.

An exact proof term for the current goal is (SepE1 EuclidPlane (λq : set ⇒ ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1) p Hp1').

We prove the intermediate claim Hpred: ∃x0 : set, ∃y0 : set, p = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3.

We use x1 to witness the existential quantifier.

We use y1 to witness the existential quantifier.

Apply and5I to the current goal.

An exact proof term for the current goal is Hp_tup1.

An exact proof term for the current goal is Hax3.

An exact proof term for the current goal is Hxb3.

An exact proof term for the current goal is Hcy3.

An exact proof term for the current goal is Hyd3.

An exact proof term for the current goal is (SepI EuclidPlane (λq : set ⇒ ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3) p HpEuclid Hpred).

Let q be given.

Assume Hq: q ∈ b3rect.

We will prove q ∈ b1 ∩ b2.

We prove the intermediate claim HqEuclid: q ∈ EuclidPlane.

An exact proof term for the current goal is (SepE1 EuclidPlane (λq0 : set ⇒ ∃x0 : set, ∃y0 : set, q0 = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3) q Hq).

We prove the intermediate claim Hqcoords: ∃xq : set, ∃yq : set, q = (xq,yq) ∧ Rlt a3 xq ∧ Rlt xq b3x ∧ Rlt c3 yq ∧ Rlt yq d3.

An exact proof term for the current goal is (SepE2 EuclidPlane (λq0 : set ⇒ ∃x0 : set, ∃y0 : set, q0 = (x0,y0) ∧ Rlt a3 x0 ∧ Rlt x0 b3x ∧ Rlt c3 y0 ∧ Rlt y0 d3) q Hq).

Apply Hqcoords to the current goal.

Let xq be given.

Assume Hqcoords2.

Apply Hqcoords2 to the current goal.

Let yq be given.

Assume Hqineq.

We prove the intermediate claim Hqtup: q = (xq,yq).

We prove the intermediate claim H1: (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq).

An exact proof term for the current goal is (andEL (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq) (Rlt yq d3) Hqineq).

We prove the intermediate claim H2: ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x).

An exact proof term for the current goal is (andEL ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) (Rlt c3 yq) H1).

We prove the intermediate claim H3: (q = (xq,yq) ∧ Rlt a3 xq).

An exact proof term for the current goal is (andEL (q = (xq,yq) ∧ Rlt a3 xq) (Rlt xq b3x) H2).

An exact proof term for the current goal is (andEL (q = (xq,yq)) (Rlt a3 xq) H3).

We prove the intermediate claim Ha3xq: Rlt a3 xq.

We prove the intermediate claim H1: (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq).

An exact proof term for the current goal is (andEL (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq) (Rlt yq d3) Hqineq).

We prove the intermediate claim H2: ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x).

An exact proof term for the current goal is (andEL ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) (Rlt c3 yq) H1).

We prove the intermediate claim H3: (q = (xq,yq) ∧ Rlt a3 xq).

An exact proof term for the current goal is (andEL (q = (xq,yq) ∧ Rlt a3 xq) (Rlt xq b3x) H2).

An exact proof term for the current goal is (andER (q = (xq,yq)) (Rlt a3 xq) H3).

We prove the intermediate claim Hxqb3: Rlt xq b3x.

We prove the intermediate claim H1: (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq).

An exact proof term for the current goal is (andEL (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq) (Rlt yq d3) Hqineq).

We prove the intermediate claim H2: ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x).

An exact proof term for the current goal is (andEL ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) (Rlt c3 yq) H1).

An exact proof term for the current goal is (andER (q = (xq,yq) ∧ Rlt a3 xq) (Rlt xq b3x) H2).

We prove the intermediate claim Hc3yq: Rlt c3 yq.

We prove the intermediate claim H1: (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq).

An exact proof term for the current goal is (andEL (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq) (Rlt yq d3) Hqineq).

An exact proof term for the current goal is (andER ((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) (Rlt c3 yq) H1).

We prove the intermediate claim Hyqd3: Rlt yq d3.

An exact proof term for the current goal is (andER (((q = (xq,yq) ∧ Rlt a3 xq) ∧ Rlt xq b3x) ∧ Rlt c3 yq) (Rlt yq d3) Hqineq).

We prove the intermediate claim Haxq: Rlt a1 xq ∧ Rlt a2 xq.

We prove the intermediate claim HxqR: xq ∈ R.

An exact proof term for the current goal is (RltE_right a3 xq Ha3xq).

We prove the intermediate claim Ha1S: SNo a1.

An exact proof term for the current goal is (real_SNo a1 Ha1R).

We prove the intermediate claim Ha2S: SNo a2.

An exact proof term for the current goal is (real_SNo a2 Ha2R).

We prove the intermediate claim Ha3xq_if: Rlt (if a1 < a2 then a2 else a1) xq.

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

An exact proof term for the current goal is Ha3xq.

Apply (SNoLt_trichotomy_or_impred a1 a2 Ha1S Ha2S (Rlt a1 xq ∧ Rlt a2 xq)) to the current goal.

Assume Ha1lt: a1 < a2.

We prove the intermediate claim Ha1a2: Rlt a1 a2.

An exact proof term for the current goal is (RltI a1 a2 Ha1R Ha2R Ha1lt).

We prove the intermediate claim Ha2xq: Rlt a2 xq.

rewrite the current goal using (If_i_1 (a1 < a2) a2 a1 Ha1lt) (from right to left).

An exact proof term for the current goal is Ha3xq_if.

We prove the intermediate claim Ha1xq: Rlt a1 xq.

An exact proof term for the current goal is (Rlt_tra a1 a2 xq Ha1a2 Ha2xq).

Apply andI to the current goal.

An exact proof term for the current goal is Ha1xq.

An exact proof term for the current goal is Ha2xq.

Assume Haeq: a1 = a2.

We prove the intermediate claim Hnlt: ¬ (a1 < a2).

Assume Hlt.

We prove the intermediate claim Hlt': a1 < a1.

rewrite the current goal using Haeq (from left to right) at position 2.

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is ((SNoLt_irref a1) Hlt').

We prove the intermediate claim Ha1xq: Rlt a1 xq.

rewrite the current goal using (If_i_0 (a1 < a2) a2 a1 Hnlt) (from right to left).

An exact proof term for the current goal is Ha3xq_if.

We prove the intermediate claim Ha2xq: Rlt a2 xq.

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

An exact proof term for the current goal is Ha1xq.

Apply andI to the current goal.

An exact proof term for the current goal is Ha1xq.

An exact proof term for the current goal is Ha2xq.

Assume Ha2lt: a2 < a1.

We prove the intermediate claim Hnlt: ¬ (a1 < a2).

Assume Hlt.

We prove the intermediate claim Ha2S': SNo a2.

An exact proof term for the current goal is Ha2S.

We prove the intermediate claim Ha1S': SNo a1.

An exact proof term for the current goal is Ha1S.

We prove the intermediate claim Ha2lt2: a2 < a2.

An exact proof term for the current goal is (SNoLt_tra a2 a1 a2 Ha2S' Ha1S' Ha2S' Ha2lt Hlt).

An exact proof term for the current goal is ((SNoLt_irref a2) Ha2lt2).

We prove the intermediate claim Ha2a1: Rlt a2 a1.

An exact proof term for the current goal is (RltI a2 a1 Ha2R Ha1R Ha2lt).

We prove the intermediate claim Ha1xq: Rlt a1 xq.

rewrite the current goal using (If_i_0 (a1 < a2) a2 a1 Hnlt) (from right to left).

An exact proof term for the current goal is Ha3xq_if.

We prove the intermediate claim Ha2xq: Rlt a2 xq.

An exact proof term for the current goal is (Rlt_tra a2 a1 xq Ha2a1 Ha1xq).

Apply andI to the current goal.

An exact proof term for the current goal is Ha1xq.

An exact proof term for the current goal is Ha2xq.

We prove the intermediate claim Hxbq: Rlt xq b1x ∧ Rlt xq b2x.

We prove the intermediate claim HxqR: xq ∈ R.

An exact proof term for the current goal is (RltE_left xq b3x Hxqb3).

We prove the intermediate claim Hb1S: SNo b1x.

An exact proof term for the current goal is (real_SNo b1x Hb1xR).

We prove the intermediate claim Hb2S: SNo b2x.

An exact proof term for the current goal is (real_SNo b2x Hb2xR).

We prove the intermediate claim HxqS: SNo xq.

An exact proof term for the current goal is (real_SNo xq HxqR).

We prove the intermediate claim Hxqb3_if: Rlt xq (if b1x < b2x then b1x else b2x).

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

An exact proof term for the current goal is Hxqb3.

Apply (SNoLt_trichotomy_or_impred b1x b2x Hb1S Hb2S (Rlt xq b1x ∧ Rlt xq b2x)) to the current goal.

Assume Hb1lt: b1x < b2x.

We prove the intermediate claim Hb1b2: Rlt b1x b2x.

An exact proof term for the current goal is (RltI b1x b2x Hb1xR Hb2xR Hb1lt).

We prove the intermediate claim Hxqb1: Rlt xq b1x.

rewrite the current goal using (If_i_1 (b1x < b2x) b1x b2x Hb1lt) (from right to left).

An exact proof term for the current goal is Hxqb3_if.

We prove the intermediate claim Hxqb2: Rlt xq b2x.

An exact proof term for the current goal is (Rlt_tra xq b1x b2x Hxqb1 Hb1b2).

Apply andI to the current goal.

An exact proof term for the current goal is Hxqb1.

An exact proof term for the current goal is Hxqb2.

Assume Hbeq: b1x = b2x.

We prove the intermediate claim Hnlt: ¬ (b1x < b2x).

Assume Hlt.

We prove the intermediate claim Hlt': b1x < b1x.

rewrite the current goal using Hbeq (from left to right) at position 2.

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is ((SNoLt_irref b1x) Hlt').

We prove the intermediate claim Hxqb2: Rlt xq b2x.

rewrite the current goal using (If_i_0 (b1x < b2x) b1x b2x Hnlt) (from right to left).

An exact proof term for the current goal is Hxqb3_if.

We prove the intermediate claim Hxqb1: Rlt xq b1x.

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

An exact proof term for the current goal is Hxqb2.

Apply andI to the current goal.

An exact proof term for the current goal is Hxqb1.

An exact proof term for the current goal is Hxqb2.

Assume Hb2lt: b2x < b1x.

We prove the intermediate claim Hnlt: ¬ (b1x < b2x).

Assume Hlt.

We prove the intermediate claim Hb2lt2: b2x < b2x.

An exact proof term for the current goal is (SNoLt_tra b2x b1x b2x Hb2S Hb1S Hb2S Hb2lt Hlt).

An exact proof term for the current goal is ((SNoLt_irref b2x) Hb2lt2).

We prove the intermediate claim Hb2b1: Rlt b2x b1x.

An exact proof term for the current goal is (RltI b2x b1x Hb2xR Hb1xR Hb2lt).

We prove the intermediate claim Hxqb2: Rlt xq b2x.

rewrite the current goal using (If_i_0 (b1x < b2x) b1x b2x Hnlt) (from right to left).

An exact proof term for the current goal is Hxqb3_if.

We prove the intermediate claim Hxqb1: Rlt xq b1x.

An exact proof term for the current goal is (Rlt_tra xq b2x b1x Hxqb2 Hb2b1).

Apply andI to the current goal.

An exact proof term for the current goal is Hxqb1.

An exact proof term for the current goal is Hxqb2.

We prove the intermediate claim Hcyq: Rlt c1 yq ∧ Rlt c2 yq.

We prove the intermediate claim HyqR: yq ∈ R.

An exact proof term for the current goal is (RltE_right c3 yq Hc3yq).

We prove the intermediate claim Hc1S: SNo c1.

An exact proof term for the current goal is (real_SNo c1 Hc1R).

We prove the intermediate claim Hc2S: SNo c2.

An exact proof term for the current goal is (real_SNo c2 Hc2R).

We prove the intermediate claim Hc3yq_if: Rlt (if c1 < c2 then c2 else c1) yq.

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

An exact proof term for the current goal is Hc3yq.

Apply (SNoLt_trichotomy_or_impred c1 c2 Hc1S Hc2S (Rlt c1 yq ∧ Rlt c2 yq)) to the current goal.

Assume Hc1lt: c1 < c2.

We prove the intermediate claim Hc1c2: Rlt c1 c2.

An exact proof term for the current goal is (RltI c1 c2 Hc1R Hc2R Hc1lt).

We prove the intermediate claim Hc2yq: Rlt c2 yq.

rewrite the current goal using (If_i_1 (c1 < c2) c2 c1 Hc1lt) (from right to left).

An exact proof term for the current goal is Hc3yq_if.

We prove the intermediate claim Hc1yq: Rlt c1 yq.

An exact proof term for the current goal is (Rlt_tra c1 c2 yq Hc1c2 Hc2yq).

Apply andI to the current goal.

An exact proof term for the current goal is Hc1yq.

An exact proof term for the current goal is Hc2yq.

Assume Hceq: c1 = c2.

We prove the intermediate claim Hnlt: ¬ (c1 < c2).

Assume Hlt.

We prove the intermediate claim Hlt': c1 < c1.

rewrite the current goal using Hceq (from left to right) at position 2.

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is ((SNoLt_irref c1) Hlt').

We prove the intermediate claim Hc1yq: Rlt c1 yq.

rewrite the current goal using (If_i_0 (c1 < c2) c2 c1 Hnlt) (from right to left).

An exact proof term for the current goal is Hc3yq_if.

We prove the intermediate claim Hc2yq: Rlt c2 yq.

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

An exact proof term for the current goal is Hc1yq.

Apply andI to the current goal.

An exact proof term for the current goal is Hc1yq.

An exact proof term for the current goal is Hc2yq.

Assume Hc2lt: c2 < c1.

We prove the intermediate claim Hnlt: ¬ (c1 < c2).

Assume Hlt.

We prove the intermediate claim Hc2lt2: c2 < c2.

An exact proof term for the current goal is (SNoLt_tra c2 c1 c2 Hc2S Hc1S Hc2S Hc2lt Hlt).

An exact proof term for the current goal is ((SNoLt_irref c2) Hc2lt2).

We prove the intermediate claim Hc2c1: Rlt c2 c1.

An exact proof term for the current goal is (RltI c2 c1 Hc2R Hc1R Hc2lt).

We prove the intermediate claim Hc1yq: Rlt c1 yq.

rewrite the current goal using (If_i_0 (c1 < c2) c2 c1 Hnlt) (from right to left).

An exact proof term for the current goal is Hc3yq_if.

We prove the intermediate claim Hc2yq: Rlt c2 yq.

An exact proof term for the current goal is (Rlt_tra c2 c1 yq Hc2c1 Hc1yq).

Apply andI to the current goal.

An exact proof term for the current goal is Hc1yq.

An exact proof term for the current goal is Hc2yq.

We prove the intermediate claim Hydq: Rlt yq d1 ∧ Rlt yq d2.

We prove the intermediate claim HyqR: yq ∈ R.

An exact proof term for the current goal is (RltE_left yq d3 Hyqd3).

We prove the intermediate claim Hd1S: SNo d1.

An exact proof term for the current goal is (real_SNo d1 Hd1R).

We prove the intermediate claim Hd2S: SNo d2.

An exact proof term for the current goal is (real_SNo d2 Hd2R).

We prove the intermediate claim HyqS: SNo yq.

An exact proof term for the current goal is (real_SNo yq HyqR).

We prove the intermediate claim Hyqd3_if: Rlt yq (if d1 < d2 then d1 else d2).

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

An exact proof term for the current goal is Hyqd3.

Apply (SNoLt_trichotomy_or_impred d1 d2 Hd1S Hd2S (Rlt yq d1 ∧ Rlt yq d2)) to the current goal.

Assume Hd1lt: d1 < d2.

We prove the intermediate claim Hd1d2: Rlt d1 d2.

An exact proof term for the current goal is (RltI d1 d2 Hd1R Hd2R Hd1lt).

We prove the intermediate claim Hyqd1: Rlt yq d1.

rewrite the current goal using (If_i_1 (d1 < d2) d1 d2 Hd1lt) (from right to left).

An exact proof term for the current goal is Hyqd3_if.

We prove the intermediate claim Hyqd2: Rlt yq d2.

An exact proof term for the current goal is (Rlt_tra yq d1 d2 Hyqd1 Hd1d2).

Apply andI to the current goal.

An exact proof term for the current goal is Hyqd1.

An exact proof term for the current goal is Hyqd2.

Assume Hdeq: d1 = d2.

We prove the intermediate claim Hnlt: ¬ (d1 < d2).

Assume Hlt.

We prove the intermediate claim Hlt': d1 < d1.

rewrite the current goal using Hdeq (from left to right) at position 2.

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is ((SNoLt_irref d1) Hlt').

We prove the intermediate claim Hyqd2: Rlt yq d2.

rewrite the current goal using (If_i_0 (d1 < d2) d1 d2 Hnlt) (from right to left).

An exact proof term for the current goal is Hyqd3_if.

We prove the intermediate claim Hyqd1: Rlt yq d1.

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

An exact proof term for the current goal is Hyqd2.

Apply andI to the current goal.

An exact proof term for the current goal is Hyqd1.

An exact proof term for the current goal is Hyqd2.

Assume Hd2lt: d2 < d1.

We prove the intermediate claim Hnlt: ¬ (d1 < d2).

Assume Hlt.

We prove the intermediate claim Hd2lt2: d2 < d2.

An exact proof term for the current goal is (SNoLt_tra d2 d1 d2 Hd2S Hd1S Hd2S Hd2lt Hlt).

An exact proof term for the current goal is ((SNoLt_irref d2) Hd2lt2).

We prove the intermediate claim Hd2d1: Rlt d2 d1.

An exact proof term for the current goal is (RltI d2 d1 Hd2R Hd1R Hd2lt).

We prove the intermediate claim Hyqd2: Rlt yq d2.

rewrite the current goal using (If_i_0 (d1 < d2) d1 d2 Hnlt) (from right to left).

An exact proof term for the current goal is Hyqd3_if.

We prove the intermediate claim Hyqd1: Rlt yq d1.

An exact proof term for the current goal is (Rlt_tra yq d2 d1 Hyqd2 Hd2d1).

Apply andI to the current goal.

An exact proof term for the current goal is Hyqd1.

An exact proof term for the current goal is Hyqd2.

We prove the intermediate claim Ha1xq: Rlt a1 xq.

An exact proof term for the current goal is (andEL (Rlt a1 xq) (Rlt a2 xq) Haxq).

We prove the intermediate claim Ha2xq: Rlt a2 xq.

An exact proof term for the current goal is (andER (Rlt a1 xq) (Rlt a2 xq) Haxq).

We prove the intermediate claim Hxqb1: Rlt xq b1x.

An exact proof term for the current goal is (andEL (Rlt xq b1x) (Rlt xq b2x) Hxbq).

We prove the intermediate claim Hxqb2: Rlt xq b2x.

An exact proof term for the current goal is (andER (Rlt xq b1x) (Rlt xq b2x) Hxbq).

We prove the intermediate claim Hc1yq: Rlt c1 yq.

An exact proof term for the current goal is (andEL (Rlt c1 yq) (Rlt c2 yq) Hcyq).

We prove the intermediate claim Hc2yq: Rlt c2 yq.

An exact proof term for the current goal is (andER (Rlt c1 yq) (Rlt c2 yq) Hcyq).

We prove the intermediate claim Hyqd1: Rlt yq d1.

An exact proof term for the current goal is (andEL (Rlt yq d1) (Rlt yq d2) Hydq).

We prove the intermediate claim Hyqd2: Rlt yq d2.

An exact proof term for the current goal is (andER (Rlt yq d1) (Rlt yq d2) Hydq).

We prove the intermediate claim Hpred1: ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1.

We use xq to witness the existential quantifier.

We use yq to witness the existential quantifier.

We prove the intermediate claim H1: q = (xq,yq) ∧ Rlt a1 xq.

An exact proof term for the current goal is (andI (q = (xq,yq)) (Rlt a1 xq) Hqtup Ha1xq).

We prove the intermediate claim H12: (q = (xq,yq) ∧ Rlt a1 xq) ∧ Rlt xq b1x.

An exact proof term for the current goal is (andI (q = (xq,yq) ∧ Rlt a1 xq) (Rlt xq b1x) H1 Hxqb1).

We prove the intermediate claim H123: ((q = (xq,yq) ∧ Rlt a1 xq) ∧ Rlt xq b1x) ∧ Rlt c1 yq.

An exact proof term for the current goal is (andI ((q = (xq,yq) ∧ Rlt a1 xq) ∧ Rlt xq b1x) (Rlt c1 yq) H12 Hc1yq).

An exact proof term for the current goal is (andI (((q = (xq,yq) ∧ Rlt a1 xq) ∧ Rlt xq b1x) ∧ Rlt c1 yq) (Rlt yq d1) H123 Hyqd1).

We prove the intermediate claim Hpred2: ∃x0 : set, ∃y0 : set, q = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2.

We use xq to witness the existential quantifier.

We use yq to witness the existential quantifier.

We prove the intermediate claim H1: q = (xq,yq) ∧ Rlt a2 xq.

An exact proof term for the current goal is (andI (q = (xq,yq)) (Rlt a2 xq) Hqtup Ha2xq).

We prove the intermediate claim H12: (q = (xq,yq) ∧ Rlt a2 xq) ∧ Rlt xq b2x.

An exact proof term for the current goal is (andI (q = (xq,yq) ∧ Rlt a2 xq) (Rlt xq b2x) H1 Hxqb2).

We prove the intermediate claim H123: ((q = (xq,yq) ∧ Rlt a2 xq) ∧ Rlt xq b2x) ∧ Rlt c2 yq.

An exact proof term for the current goal is (andI ((q = (xq,yq) ∧ Rlt a2 xq) ∧ Rlt xq b2x) (Rlt c2 yq) H12 Hc2yq).

An exact proof term for the current goal is (andI (((q = (xq,yq) ∧ Rlt a2 xq) ∧ Rlt xq b2x) ∧ Rlt c2 yq) (Rlt yq d2) H123 Hyqd2).

We prove the intermediate claim Hqb1: q ∈ b1.

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

An exact proof term for the current goal is (SepI EuclidPlane (λq0 : set ⇒ ∃x0 : set, ∃y0 : set, q0 = (x0,y0) ∧ Rlt a1 x0 ∧ Rlt x0 b1x ∧ Rlt c1 y0 ∧ Rlt y0 d1) q HqEuclid Hpred1).

We prove the intermediate claim Hqb2: q ∈ b2.

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

An exact proof term for the current goal is (SepI EuclidPlane (λq0 : set ⇒ ∃x0 : set, ∃y0 : set, q0 = (x0,y0) ∧ Rlt a2 x0 ∧ Rlt x0 b2x ∧ Rlt c2 y0 ∧ Rlt y0 d2) q HqEuclid Hpred2).

An exact proof term for the current goal is (binintersectI b1 b2 q Hqb1 Hqb2).