Let x, c1, c2, r1 and r2 be given.
Assume Hx: x ∈ EuclidPlane.
Assume Hc1: c1 ∈ EuclidPlane.
Assume Hc2: c2 ∈ EuclidPlane.
Assume Hr1: Rlt 0 r1.
Assume Hr2: Rlt 0 r2.
Assume Hx1: Rlt (distance_R2 x c1) r1.
Assume Hx2: Rlt (distance_R2 x c2) r2.
Set d1 to be the term distance_R2 x c1.
Set d2 to be the term distance_R2 x c2.
We prove the intermediate claim Hd1R: d1 ∈ R.
An exact proof term for the current goal is (distance_R2_in_R x c1 Hx Hc1).
We prove the intermediate claim Hd2R: d2 ∈ R.
An exact proof term for the current goal is (distance_R2_in_R x c2 Hx Hc2).
We prove the intermediate claim Hr1R: r1 ∈ R.
An exact proof term for the current goal is (RltE_right 0 r1 Hr1).
We prove the intermediate claim Hr2R: r2 ∈ R.
An exact proof term for the current goal is (RltE_right 0 r2 Hr2).
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 Hr1S: SNo r1.
An exact proof term for the current goal is (real_SNo r1 Hr1R).
We prove the intermediate claim Hr2S: SNo r2.
An exact proof term for the current goal is (real_SNo r2 Hr2R).
Set m1 to be the term add_SNo r1 (minus_SNo d1).
Set m2 to be the term add_SNo r2 (minus_SNo d2).
We prove the intermediate claim Hm1R: m1 ∈ R.
An exact proof term for the current goal is (real_add_SNo r1 Hr1R (minus_SNo d1) (real_minus_SNo d1 Hd1R)).
We prove the intermediate claim Hm2R: m2 ∈ R.
An exact proof term for the current goal is (real_add_SNo r2 Hr2R (minus_SNo d2) (real_minus_SNo d2 Hd2R)).
We prove the intermediate claim Hm1S: SNo m1.
An exact proof term for the current goal is (real_SNo m1 Hm1R).
We prove the intermediate claim Hm2S: SNo m2.
An exact proof term for the current goal is (real_SNo m2 Hm2R).
We prove the intermediate claim Hd1lt: d1 < r1.
An exact proof term for the current goal is (RltE_lt d1 r1 Hx1).
We prove the intermediate claim Hd2lt: d2 < r2.
An exact proof term for the current goal is (RltE_lt d2 r2 Hx2).
We prove the intermediate claim Hm1posS: 0 < m1.
An exact proof term for the current goal is (SNoLt_minus_pos d1 r1 Hd1S Hr1S Hd1lt).
We prove the intermediate claim Hm2posS: 0 < m2.
An exact proof term for the current goal is (SNoLt_minus_pos d2 r2 Hd2S Hr2S Hd2lt).
We prove the intermediate claim Hm1pos: Rlt 0 m1.
An exact proof term for the current goal is (RltI 0 m1 real_0 Hm1R Hm1posS).
We prove the intermediate claim Hm2pos: Rlt 0 m2.
An exact proof term for the current goal is (RltI 0 m2 real_0 Hm2R Hm2posS).
Apply (exists_eps_lt_two_pos_Euclid m1 m2 Hm1R Hm2R Hm1pos Hm2pos) to the current goal.
Let r3 be given.
Assume Hr3core.
We prove the intermediate claim Hr3Left1: (r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1.
An exact proof term for the current goal is (andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) (Rlt r3 m2) Hr3core).
We prove the intermediate claim Hr3m2: Rlt r3 m2.
An exact proof term for the current goal is (andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) (Rlt r3 m2) Hr3core).
We prove the intermediate claim Hr3pair: r3 ∈ R ∧ Rlt 0 r3.
An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 m1) Hr3Left1).
We prove the intermediate claim Hr3m1: Rlt r3 m1.
An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 m1) Hr3Left1).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (andEL (r3 ∈ R) (Rlt 0 r3) Hr3pair).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (andER (r3 ∈ R) (Rlt 0 r3) Hr3pair).
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3pos.
Let p be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hpx: Rlt (distance_R2 p x) r3.
We will prove Rlt (distance_R2 p c1) r1 ∧ Rlt (distance_R2 p c2) r2.
Apply andI to the current goal.
Set dpx to be the term distance_R2 p x.
We prove the intermediate claim HdpxR: dpx ∈ R.
An exact proof term for the current goal is (distance_R2_in_R p x Hp Hx).
We prove the intermediate claim HdpxS: SNo dpx.
An exact proof term for the current goal is (real_SNo dpx HdpxR).
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 Hpxlt: dpx < r3.
An exact proof term for the current goal is (RltE_lt dpx r3 Hpx).
We prove the intermediate claim Hdpxm1: Rlt dpx m1.
An exact proof term for the current goal is (Rlt_tra dpx r3 m1 Hpx Hr3m1).
We prove the intermediate claim Hdpxm1lt: dpx < m1.
An exact proof term for the current goal is (RltE_lt dpx m1 Hdpxm1).
We prove the intermediate claim HsumLt: Rlt (add_SNo dpx d1) r1.
We will prove Rlt (add_SNo dpx d1) r1.
We prove the intermediate claim HsumS: SNo (add_SNo d1 dpx).
An exact proof term for the current goal is (real_SNo (add_SNo d1 dpx) (real_add_SNo d1 Hd1R dpx HdpxR)).
We prove the intermediate claim HsumS2: SNo (add_SNo dpx d1).
An exact proof term for the current goal is (real_SNo (add_SNo dpx d1) (real_add_SNo dpx HdpxR d1 Hd1R)).
We prove the intermediate claim HtmpS: add_SNo d1 dpx < add_SNo d1 m1.
An exact proof term for the current goal is (add_SNo_Lt2 d1 dpx m1 Hd1S HdpxS Hm1S Hdpxm1lt).
We prove the intermediate claim HtmpR: Rlt (add_SNo d1 dpx) (add_SNo d1 m1).
An exact proof term for the current goal is (RltI (add_SNo d1 dpx) (add_SNo d1 m1) (real_add_SNo d1 Hd1R dpx HdpxR) (real_add_SNo d1 Hd1R m1 Hm1R) HtmpS).
We prove the intermediate claim Heq: add_SNo d1 m1 = r1.
We will prove add_SNo d1 m1 = r1.
We prove the intermediate claim Hmd1S: SNo (minus_SNo d1).
An exact proof term for the current goal is (SNo_minus_SNo d1 Hd1S).
We prove the intermediate claim Hassoc1: add_SNo d1 (add_SNo r1 (minus_SNo d1)) = add_SNo (add_SNo d1 r1) (minus_SNo d1).
An exact proof term for the current goal is (add_SNo_assoc d1 r1 (minus_SNo d1) Hd1S Hr1S Hmd1S).
We prove the intermediate claim Hcom1: add_SNo d1 r1 = add_SNo r1 d1.
An exact proof term for the current goal is (add_SNo_com d1 r1 Hd1S Hr1S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo r1 d1) (minus_SNo d1) = add_SNo r1 (add_SNo d1 (minus_SNo d1)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc r1 d1 (minus_SNo d1) Hr1S Hd1S Hmd1S).
We prove the intermediate claim Hinv: add_SNo d1 (minus_SNo d1) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv d1 Hd1S).
We will prove add_SNo d1 m1 = r1.
We prove the intermediate claim Hm1Def: m1 = add_SNo r1 (minus_SNo d1).
Use reflexivity.
rewrite the current goal using Hm1Def (from left to right).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R r1 Hr1S).
rewrite the current goal using (add_SNo_com dpx d1 HdpxS Hd1S) (from left to right) at position 1.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HtmpR.
We prove the intermediate claim Htri: Rle (distance_R2 p c1) (add_SNo dpx d1).
An exact proof term for the current goal is (distance_R2_triangle_Rle p x c1 Hp Hx Hc1).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (distance_R2 p c1) (add_SNo dpx d1) r1 Htri HsumLt).
Set dpx to be the term distance_R2 p x.
We prove the intermediate claim HdpxR: dpx ∈ R.
An exact proof term for the current goal is (distance_R2_in_R p x Hp Hx).
We prove the intermediate claim HdpxS: SNo dpx.
An exact proof term for the current goal is (real_SNo dpx HdpxR).
We prove the intermediate claim Hdpxm2: Rlt dpx m2.
An exact proof term for the current goal is (Rlt_tra dpx r3 m2 Hpx Hr3m2).
We prove the intermediate claim Hdpxm2lt: dpx < m2.
An exact proof term for the current goal is (RltE_lt dpx m2 Hdpxm2).
We prove the intermediate claim HsumLt: Rlt (add_SNo dpx d2) r2.
We will prove Rlt (add_SNo dpx d2) r2.
We prove the intermediate claim HtmpS: add_SNo d2 dpx < add_SNo d2 m2.
An exact proof term for the current goal is (add_SNo_Lt2 d2 dpx m2 Hd2S HdpxS Hm2S Hdpxm2lt).
We prove the intermediate claim HtmpR: Rlt (add_SNo d2 dpx) (add_SNo d2 m2).
An exact proof term for the current goal is (RltI (add_SNo d2 dpx) (add_SNo d2 m2) (real_add_SNo d2 Hd2R dpx HdpxR) (real_add_SNo d2 Hd2R m2 Hm2R) HtmpS).
We prove the intermediate claim Heq: add_SNo d2 m2 = r2.
We will prove add_SNo d2 m2 = r2.
We prove the intermediate claim Hmd2S: SNo (minus_SNo d2).
An exact proof term for the current goal is (SNo_minus_SNo d2 Hd2S).
We prove the intermediate claim Hassoc1: add_SNo d2 (add_SNo r2 (minus_SNo d2)) = add_SNo (add_SNo d2 r2) (minus_SNo d2).
An exact proof term for the current goal is (add_SNo_assoc d2 r2 (minus_SNo d2) Hd2S Hr2S Hmd2S).
We prove the intermediate claim Hcom1: add_SNo d2 r2 = add_SNo r2 d2.
An exact proof term for the current goal is (add_SNo_com d2 r2 Hd2S Hr2S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo r2 d2) (minus_SNo d2) = add_SNo r2 (add_SNo d2 (minus_SNo d2)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc r2 d2 (minus_SNo d2) Hr2S Hd2S Hmd2S).
We prove the intermediate claim Hinv: add_SNo d2 (minus_SNo d2) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv d2 Hd2S).
We will prove add_SNo d2 m2 = r2.
We prove the intermediate claim Hm2Def: m2 = add_SNo r2 (minus_SNo d2).
Use reflexivity.
rewrite the current goal using Hm2Def (from left to right).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R r2 Hr2S).
rewrite the current goal using (add_SNo_com dpx d2 HdpxS Hd2S) (from left to right) at position 1.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HtmpR.
We prove the intermediate claim Htri: Rle (distance_R2 p c2) (add_SNo dpx d2).
An exact proof term for the current goal is (distance_R2_triangle_Rle p x c2 Hp Hx Hc2).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (distance_R2 p c2) (add_SNo dpx d2) r2 Htri HsumLt).
∎