Let x, c and r0 be given.
Assume Hx: x ∈ EuclidPlane.
Assume Hc: c ∈ EuclidPlane.
Assume Hr0: Rlt 0 r0.
Assume Hxc: Rlt (distance_R2 x c) r0.
Set x0 to be the term R2_xcoord x.
Set y0 to be the term R2_ycoord x.
Set dxc to be the term distance_R2 x c.
We prove the intermediate claim Hr0R: r0 ∈ R.
An exact proof term for the current goal is (RltE_right 0 r0 Hr0).
We prove the intermediate claim HdxcR: dxc ∈ R.
An exact proof term for the current goal is (distance_R2_in_R x c Hx Hc).
We prove the intermediate claim Hr0S: SNo r0.
An exact proof term for the current goal is (real_SNo r0 Hr0R).
We prove the intermediate claim HdxcS: SNo dxc.
An exact proof term for the current goal is (real_SNo dxc HdxcR).
Set diff to be the term add_SNo r0 (minus_SNo dxc).
We prove the intermediate claim HdiffR: diff ∈ R.
An exact proof term for the current goal is (real_add_SNo r0 Hr0R (minus_SNo dxc) (real_minus_SNo dxc HdxcR)).
We prove the intermediate claim HdiffPos: Rlt 0 diff.
An exact proof term for the current goal is (Rlt_0_diff_of_lt dxc r0 Hxc).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < diff.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid diff HdiffR HdiffPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < diff) HNpair).
We prove the intermediate claim HepsLtDiffS: eps_ N < diff.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < diff) HNpair).
Set eps to be the term eps_ N.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HsumLtS: add_SNo dxc eps < r0.
We prove the intermediate claim HdiffS: SNo diff.
An exact proof term for the current goal is (real_SNo diff HdiffR).
We prove the intermediate claim HepsLtR: Rlt eps diff.
An exact proof term for the current goal is (RltI eps diff HepsR HdiffR HepsLtDiffS).
We prove the intermediate claim HepsLt: eps < diff.
An exact proof term for the current goal is (RltE_lt eps diff HepsLtR).
We prove the intermediate claim Hdxc_eps_lt: add_SNo dxc eps < add_SNo dxc diff.
An exact proof term for the current goal is (add_SNo_Lt2 dxc eps diff HdxcS HepsS HdiffS HepsLt).
We prove the intermediate claim HdxcDiffEq: add_SNo dxc diff = r0.
We will prove add_SNo dxc diff = r0.
rewrite the current goal using (add_SNo_assoc dxc r0 (minus_SNo dxc) HdxcS Hr0S (SNo_minus_SNo dxc HdxcS)) (from left to right).
rewrite the current goal using (add_SNo_com dxc r0 HdxcS Hr0S) (from left to right).
rewrite the current goal using (add_SNo_assoc r0 dxc (minus_SNo dxc) Hr0S HdxcS (SNo_minus_SNo dxc HdxcS)) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv dxc HdxcS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R r0 Hr0S).
rewrite the current goal using HdxcDiffEq (from right to left).
An exact proof term for the current goal is Hdxc_eps_lt.
We prove the intermediate claim HsumLt: Rlt (add_SNo dxc eps) r0.
We prove the intermediate claim HsumR: add_SNo dxc eps ∈ R.
An exact proof term for the current goal is (real_add_SNo dxc HdxcR eps HepsR).
An exact proof term for the current goal is (RltI (add_SNo dxc eps) r0 HsumR Hr0R HsumLtS).
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
Set r3 to be the term eps_ (ordsucc N).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
We prove the intermediate claim Hr3PosS: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N) HsuccOmega).
We prove the intermediate claim Hr3Pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R Hr3PosS).
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim Hr3Half: add_SNo r3 r3 = eps.
An exact proof term for the current goal is (eps_ordsucc_half_add N HNnat).
Set a to be the term add_SNo x0 (minus_SNo r3).
Set b to be the term add_SNo x0 r3.
Set c1 to be the term add_SNo y0 (minus_SNo r3).
Set d1 to be the term add_SNo y0 r3.
Set Rect to be the term {p ∈ EuclidPlane|∃x1 y1 : set, p = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b ∧ Rlt c1 y1 ∧ Rlt y1 d1}.
We prove the intermediate claim Hx0R: x0 ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R x Hx).
We prove the intermediate claim Hy0R: y0 ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R x Hx).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0R).
We prove the intermediate claim Hy0S: SNo y0.
An exact proof term for the current goal is (real_SNo y0 Hy0R).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (real_add_SNo x0 Hx0R (minus_SNo r3) (real_minus_SNo r3 Hr3R)).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (real_add_SNo x0 Hx0R r3 Hr3R).
We prove the intermediate claim Hc1R: c1 ∈ R.
An exact proof term for the current goal is (real_add_SNo y0 Hy0R (minus_SNo r3) (real_minus_SNo r3 Hr3R)).
We prove the intermediate claim Hd1R: d1 ∈ R.
An exact proof term for the current goal is (real_add_SNo y0 Hy0R r3 Hr3R).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 Hd1S: SNo d1.
An exact proof term for the current goal is (real_SNo d1 Hd1R).
We prove the intermediate claim Hm_r3_lt_0: minus_SNo r3 < 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 r3 SNo_0 Hr3S Hr3PosS).
We prove the intermediate claim Hm_r3S: SNo (minus_SNo r3).
An exact proof term for the current goal is (SNo_minus_SNo r3 Hr3S).
We prove the intermediate claim Hm_r3_lt_r3: minus_SNo r3 < r3.
An exact proof term for the current goal is (SNoLt_tra (minus_SNo r3) 0 r3 Hm_r3S SNo_0 Hr3S Hm_r3_lt_0 Hr3PosS).
We prove the intermediate claim HabSlt: a < b.
We prove the intermediate claim Htmp: add_SNo x0 (minus_SNo r3) < add_SNo x0 r3.
An exact proof term for the current goal is (add_SNo_Lt2 x0 (minus_SNo r3) r3 Hx0S Hm_r3S Hr3S Hm_r3_lt_r3).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HcdSlt: c1 < d1.
We prove the intermediate claim Htmp: add_SNo y0 (minus_SNo r3) < add_SNo y0 r3.
An exact proof term for the current goal is (add_SNo_Lt2 y0 (minus_SNo r3) r3 Hy0S Hm_r3S Hr3S Hm_r3_lt_r3).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HabRlt: Rlt a b.
An exact proof term for the current goal is (RltI a b HaR HbR HabSlt).
We prove the intermediate claim HcdRlt: Rlt c1 d1.
An exact proof term for the current goal is (RltI c1 d1 Hc1R Hd1R HcdSlt).
We prove the intermediate claim HRect: Rect ∈ rectangular_regions.
An exact proof term for the current goal is (rectangular_regionI a b c1 d1 HaR HbR Hc1R Hd1R HabRlt HcdRlt).
We prove the intermediate claim Hx_in_Rect: x ∈ Rect.
rewrite the current goal using (EuclidPlane_eta x Hx) (from right to left) at position 1.
We prove the intermediate claim HxyE: (x0,y0) ∈ EuclidPlane.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x0 y0 Hx0R Hy0R).
Apply (SepI EuclidPlane (λp0 : set ⇒ ∃x1 y1 : set, p0 = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b ∧ Rlt c1 y1 ∧ Rlt y1 d1) (x0,y0) HxyE) to the current goal.
We use x0 to witness the existential quantifier.
We use y0 to witness the existential quantifier.
We prove the intermediate claim Hax0: Rlt a x0.
We prove the intermediate claim Hx0plus0: add_SNo x0 0 = x0.
An exact proof term for the current goal is (add_SNo_0R x0 Hx0S).
We prove the intermediate claim Hax0S': add_SNo x0 (minus_SNo r3) < add_SNo x0 0.
An exact proof term for the current goal is (add_SNo_Lt2 x0 (minus_SNo r3) 0 Hx0S Hm_r3S SNo_0 Hm_r3_lt_0).
We prove the intermediate claim Hax0Eq: add_SNo x0 (minus_SNo r3) = a.
Use reflexivity.
We prove the intermediate claim Hax0S: a < x0.
rewrite the current goal using Hax0Eq (from right to left).
rewrite the current goal using Hx0plus0 (from right to left) at position 2.
An exact proof term for the current goal is Hax0S'.
rewrite the current goal using Hax0Eq (from right to left) at position 1.
An exact proof term for the current goal is (RltI (add_SNo x0 (minus_SNo r3)) x0 HaR Hx0R Hax0S).
We prove the intermediate claim Hx0b: Rlt x0 b.
We prove the intermediate claim Hx0bS: x0 < add_SNo x0 r3.
An exact proof term for the current goal is (add_SNo_eps_Lt x0 Hx0S (ordsucc N) HsuccOmega).
An exact proof term for the current goal is (RltI x0 b Hx0R HbR Hx0bS).
We prove the intermediate claim Hcy0: Rlt c1 y0.
We prove the intermediate claim Hy0plus0: add_SNo y0 0 = y0.
An exact proof term for the current goal is (add_SNo_0R y0 Hy0S).
We prove the intermediate claim Hcy0S': add_SNo y0 (minus_SNo r3) < add_SNo y0 0.
An exact proof term for the current goal is (add_SNo_Lt2 y0 (minus_SNo r3) 0 Hy0S Hm_r3S SNo_0 Hm_r3_lt_0).
We prove the intermediate claim Hcy0Eq: add_SNo y0 (minus_SNo r3) = c1.
Use reflexivity.
We prove the intermediate claim Hcy0S: c1 < y0.
rewrite the current goal using Hcy0Eq (from right to left).
rewrite the current goal using Hy0plus0 (from right to left) at position 2.
An exact proof term for the current goal is Hcy0S'.
rewrite the current goal using Hcy0Eq (from right to left) at position 1.
An exact proof term for the current goal is (RltI (add_SNo y0 (minus_SNo r3)) y0 Hc1R Hy0R Hcy0S).
We prove the intermediate claim Hy0d: Rlt y0 d1.
We prove the intermediate claim Hy0dS: y0 < add_SNo y0 r3.
An exact proof term for the current goal is (add_SNo_eps_Lt y0 Hy0S (ordsucc N) HsuccOmega).
An exact proof term for the current goal is (RltI y0 d1 Hy0R Hd1R Hy0dS).
We prove the intermediate claim Hrefl: (x0,y0) = (x0,y0).
Use reflexivity.
We prove the intermediate claim Hpair: (x0,y0) = (x0,y0) ∧ Rlt a x0.
An exact proof term for the current goal is (andI ((x0,y0) = (x0,y0)) (Rlt a x0) Hrefl Hax0).
We prove the intermediate claim H1: ((x0,y0) = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b.
An exact proof term for the current goal is (andI ((x0,y0) = (x0,y0) ∧ Rlt a x0) (Rlt x0 b) Hpair Hx0b).
We prove the intermediate claim H2: (((x0,y0) = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b) ∧ Rlt c1 y0.
An exact proof term for the current goal is (andI (((x0,y0) = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b) (Rlt c1 y0) H1 Hcy0).
An exact proof term for the current goal is (andI ((((x0,y0) = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b) ∧ Rlt c1 y0) (Rlt y0 d1) H2 Hy0d).
We prove the intermediate claim HRectSub: Rect ⊆ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r0}.
Let p be given.
Assume HpRect: p ∈ Rect.
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ ∃x1 y1 : set, p0 = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b ∧ Rlt c1 y1 ∧ Rlt y1 d1) p HpRect).
We prove the intermediate claim HpPred: ∃x1 y1 : set, p = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b ∧ Rlt c1 y1 ∧ Rlt y1 d1.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ ∃x1 y1 : set, p0 = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b ∧ Rlt c1 y1 ∧ Rlt y1 d1) p HpRect).
Apply HpPred to the current goal.
Let x1 be given.
Assume HpPred2.
Apply HpPred2 to the current goal.
Let y1 be given.
Assume HpCore.
We prove the intermediate claim Hcore1: (((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b) ∧ Rlt c1 y1).
An exact proof term for the current goal is (andEL (((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b) ∧ Rlt c1 y1) (Rlt y1 d1) HpCore).
We prove the intermediate claim Hy1d: Rlt y1 d1.
An exact proof term for the current goal is (andER (((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b) ∧ Rlt c1 y1) (Rlt y1 d1) HpCore).
We prove the intermediate claim Hcore2: ((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b).
An exact proof term for the current goal is (andEL ((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b) (Rlt c1 y1) Hcore1).
We prove the intermediate claim Hcy1: Rlt c1 y1.
An exact proof term for the current goal is (andER ((p = (x1,y1) ∧ Rlt a x1) ∧ Rlt x1 b) (Rlt c1 y1) Hcore1).
We prove the intermediate claim Hcore3: (p = (x1,y1) ∧ Rlt a x1).
An exact proof term for the current goal is (andEL (p = (x1,y1) ∧ Rlt a x1) (Rlt x1 b) Hcore2).
We prove the intermediate claim Hx1b: Rlt x1 b.
An exact proof term for the current goal is (andER (p = (x1,y1) ∧ Rlt a x1) (Rlt x1 b) Hcore2).
We prove the intermediate claim HpEq: p = (x1,y1).
An exact proof term for the current goal is (andEL (p = (x1,y1)) (Rlt a x1) Hcore3).
We prove the intermediate claim Hax1: Rlt a x1.
An exact proof term for the current goal is (andER (p = (x1,y1)) (Rlt a x1) Hcore3).
We prove the intermediate claim HxpEq: R2_xcoord p = x1.
rewrite the current goal using HpEq (from left to right) at position 1.
An exact proof term for the current goal is (R2_xcoord_tuple x1 y1).
We prove the intermediate claim HypEq: R2_ycoord p = y1.
rewrite the current goal using HpEq (from left to right) at position 1.
An exact proof term for the current goal is (R2_ycoord_tuple x1 y1).
We prove the intermediate claim Hx1R: x1 ∈ R.
rewrite the current goal using HxpEq (from right to left) at position 1.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R p HpE).
We prove the intermediate claim Hy1R: y1 ∈ R.
rewrite the current goal using HypEq (from right to left) at position 1.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R p HpE).
We prove the intermediate claim HabsdxLt: abs_SNo (add_SNo (R2_xcoord p) (minus_SNo x0)) < r3.
rewrite the current goal using HxpEq (from left to right) at position 1.
An exact proof term for the current goal is (abs_diff_lt_of_between x1 x0 r3 Hx1R Hx0R Hr3R Hr3Pos Hax1 Hx1b).
We prove the intermediate claim HabsdyLt: abs_SNo (add_SNo (R2_ycoord p) (minus_SNo y0)) < r3.
rewrite the current goal using HypEq (from left to right) at position 1.
An exact proof term for the current goal is (abs_diff_lt_of_between y1 y0 r3 Hy1R Hy0R Hr3R Hr3Pos Hcy1 Hy1d).
Set axp to be the term abs_SNo (add_SNo (R2_xcoord p) (minus_SNo x0)).
Set ayp to be the term abs_SNo (add_SNo (R2_ycoord p) (minus_SNo y0)).
We prove the intermediate claim HaxpS: SNo axp.
An exact proof term for the current goal is (SNo_abs_SNo (add_SNo (R2_xcoord p) (minus_SNo x0)) (real_SNo (add_SNo (R2_xcoord p) (minus_SNo x0)) (real_add_SNo (R2_xcoord p) (EuclidPlane_xcoord_in_R p HpE) (minus_SNo x0) (real_minus_SNo x0 Hx0R)))).
We prove the intermediate claim HaypS: SNo ayp.
An exact proof term for the current goal is (SNo_abs_SNo (add_SNo (R2_ycoord p) (minus_SNo y0)) (real_SNo (add_SNo (R2_ycoord p) (minus_SNo y0)) (real_add_SNo (R2_ycoord p) (EuclidPlane_ycoord_in_R p HpE) (minus_SNo y0) (real_minus_SNo y0 Hy0R)))).
We prove the intermediate claim HsumAbsLt: add_SNo axp ayp < eps.
We prove the intermediate claim HsumLt0: add_SNo axp ayp < add_SNo r3 r3.
An exact proof term for the current goal is (add_SNo_Lt3 axp ayp r3 r3 HaxpS HaypS Hr3S Hr3S HabsdxLt HabsdyLt).
rewrite the current goal using Hr3Half (from right to left).
An exact proof term for the current goal is HsumLt0.
We prove the intermediate claim HdistLeSum: distance_R2 p x ≤ add_SNo axp ayp.
An exact proof term for the current goal is (distance_R2_le_absdx_plus_absdy p x HpE Hx).
We prove the intermediate claim HdistS: SNo (distance_R2 p x).
An exact proof term for the current goal is (real_SNo (distance_R2 p x) (distance_R2_in_R p x HpE Hx)).
We prove the intermediate claim HepsS2: SNo eps.
An exact proof term for the current goal is HepsS.
We prove the intermediate claim HdistLtEpsS: distance_R2 p x < eps.
An exact proof term for the current goal is (SNoLeLt_tra (distance_R2 p x) (add_SNo axp ayp) eps HdistS (SNo_add_SNo axp ayp HaxpS HaypS) HepsS2 HdistLeSum HsumAbsLt).
We prove the intermediate claim HdistLtEps: Rlt (distance_R2 p x) eps.
An exact proof term for the current goal is (RltI (distance_R2 p x) eps (distance_R2_in_R p x HpE Hx) HepsR HdistLtEpsS).
We prove the intermediate claim Htri: Rle (distance_R2 p c) (add_SNo (distance_R2 p x) dxc).
An exact proof term for the current goal is (distance_R2_triangle_Rle p x c HpE Hx Hc).
We prove the intermediate claim HdistLtEpsS2: distance_R2 p x < eps.
An exact proof term for the current goal is HdistLtEpsS.
We prove the intermediate claim Hsum2Lt: add_SNo (distance_R2 p x) dxc < r0.
We prove the intermediate claim Hcom: add_SNo (distance_R2 p x) dxc = add_SNo dxc (distance_R2 p x).
An exact proof term for the current goal is (add_SNo_com (distance_R2 p x) dxc (real_SNo (distance_R2 p x) (distance_R2_in_R p x HpE Hx)) HdxcS).
rewrite the current goal using Hcom (from left to right).
We prove the intermediate claim Htmp: add_SNo dxc (distance_R2 p x) < add_SNo dxc eps.
An exact proof term for the current goal is (add_SNo_Lt2 dxc (distance_R2 p x) eps HdxcS (real_SNo (distance_R2 p x) (distance_R2_in_R p x HpE Hx)) HepsS HdistLtEpsS2).
We prove the intermediate claim HsumEq: add_SNo dxc eps = add_SNo dxc eps.
Use reflexivity.
An exact proof term for the current goal is (SNoLt_tra (add_SNo dxc (distance_R2 p x)) (add_SNo dxc eps) r0 (SNo_add_SNo dxc (distance_R2 p x) HdxcS (real_SNo (distance_R2 p x) (distance_R2_in_R p x HpE Hx))) (SNo_add_SNo dxc eps HdxcS HepsS) Hr0S Htmp HsumLtS).
We prove the intermediate claim Hsum2Rlt: Rlt (add_SNo (distance_R2 p x) dxc) r0.
An exact proof term for the current goal is (RltI (add_SNo (distance_R2 p x) dxc) r0 (real_add_SNo (distance_R2 p x) (distance_R2_in_R p x HpE Hx) dxc HdxcR) Hr0R Hsum2Lt).
We prove the intermediate claim HpcLt: Rlt (distance_R2 p c) r0.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (distance_R2 p c) (add_SNo (distance_R2 p x) dxc) r0 Htri Hsum2Rlt).
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r0) p HpE HpcLt).
We use Rect to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HRect.
Apply andI to the current goal.
An exact proof term for the current goal is Hx_in_Rect.
An exact proof term for the current goal is HRectSub.
∎