Let p and c be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hc: c ∈ EuclidPlane.
Set dx to be the term add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord c)).
Set dy to be the term add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord c)).
Set ax to be the term abs_SNo dx.
Set ay to be the term abs_SNo dy.
Set s to be the term add_SNo ax ay.
Set d to be the term distance_R2 p c.
We prove the intermediate claim HpxR: R2_xcoord p ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R p Hp).
We prove the intermediate claim HpyR: R2_ycoord p ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R p Hp).
We prove the intermediate claim HcxR: R2_xcoord c ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R c Hc).
We prove the intermediate claim HcyR: R2_ycoord c ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R c Hc).
We prove the intermediate claim HmxR: minus_SNo (R2_xcoord c) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_xcoord c) HcxR).
We prove the intermediate claim HmyR: minus_SNo (R2_ycoord c) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_ycoord c) HcyR).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_xcoord p) HpxR (minus_SNo (R2_xcoord c)) HmxR).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_ycoord p) HpyR (minus_SNo (R2_ycoord c)) HmyR).
We prove the intermediate claim HdxS: SNo dx.
An exact proof term for the current goal is (real_SNo dx HdxR).
We prove the intermediate claim HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
We prove the intermediate claim HaxS: SNo ax.
An exact proof term for the current goal is (SNo_abs_SNo dx HdxS).
We prove the intermediate claim HayS: SNo ay.
An exact proof term for the current goal is (SNo_abs_SNo dy HdyS).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (distance_R2_in_R p c Hp Hc).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (SNo_add_SNo ax ay HaxS HayS).
We prove the intermediate claim HaxNN: 0 ≤ ax.
An exact proof term for the current goal is (abs_SNo_nonneg dx HdxS).
We prove the intermediate claim HayNN: 0 ≤ ay.
An exact proof term for the current goal is (abs_SNo_nonneg dy HdyS).
We prove the intermediate claim HdNN: 0 ≤ d.
An exact proof term for the current goal is (distance_R2_nonneg p c Hp Hc).
We prove the intermediate claim HsNN: 0 ≤ s.
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le3 0 0 ax ay SNo_0 SNo_0 HaxS HayS HaxNN HayNN).
Set ax2 to be the term mul_SNo ax ax.
Set ay2 to be the term mul_SNo ay ay.
Set d2 to be the term mul_SNo d d.
Set s2 to be the term mul_SNo s s.
We prove the intermediate claim Hax2S: SNo ax2.
An exact proof term for the current goal is (SNo_mul_SNo ax ax HaxS HaxS).
We prove the intermediate claim Hay2S: SNo ay2.
An exact proof term for the current goal is (SNo_mul_SNo ay ay HayS HayS).
We prove the intermediate claim Hd2S: SNo d2.
An exact proof term for the current goal is (SNo_mul_SNo d d HdS HdS).
We prove the intermediate claim Hs2S: SNo s2.
An exact proof term for the current goal is (SNo_mul_SNo s s HsS HsS).
We prove the intermediate claim Hd2Eq: d2 = add_SNo ax2 ay2.
We will prove d2 = add_SNo ax2 ay2.
We prove the intermediate claim Hd2Def: d2 = mul_SNo (distance_R2 p c) (distance_R2 p c).
Use reflexivity.
rewrite the current goal using Hd2Def (from left to right) at position 1.
We prove the intermediate claim Hdsqr: mul_SNo (distance_R2 p c) (distance_R2 p c) = add_SNo (mul_SNo dx dx) (mul_SNo dy dy).
An exact proof term for the current goal is (distance_R2_sqr p c Hp Hc).
rewrite the current goal using Hdsqr (from left to right).
rewrite the current goal using (abs_SNo_sqr_eq dx HdxS) (from right to left) at position 1.
rewrite the current goal using (abs_SNo_sqr_eq dy HdyS) (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hs2Eq: s2 = add_SNo ax2 (add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2)).
We will prove s2 = add_SNo ax2 (add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2)).
rewrite the current goal using (SNo_foil ax ay ax ay HaxS HayS HaxS HayS) (from right to left).
Use reflexivity.
We prove the intermediate claim Hm1S: SNo (mul_SNo ax ay).
An exact proof term for the current goal is (SNo_mul_SNo ax ay HaxS HayS).
We prove the intermediate claim Hm2S: SNo (mul_SNo ay ax).
An exact proof term for the current goal is (SNo_mul_SNo ay ax HayS HaxS).
We prove the intermediate claim Hm1NN: 0 ≤ mul_SNo ax ay.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg ax ay HaxS HayS HaxNN HayNN).
We prove the intermediate claim Hm2NN: 0 ≤ mul_SNo ay ax.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg ay ax HayS HaxS HayNN HaxNN).
We prove the intermediate claim Hay2_le_m2ay2: ay2 ≤ add_SNo (mul_SNo ay ax) ay2.
We prove the intermediate claim H0le_m2: 0 ≤ mul_SNo ay ax.
An exact proof term for the current goal is Hm2NN.
We prove the intermediate claim Htmp: add_SNo 0 ay2 ≤ add_SNo (mul_SNo ay ax) ay2.
An exact proof term for the current goal is (add_SNo_Le1 0 ay2 (mul_SNo ay ax) SNo_0 Hay2S Hm2S H0le_m2).
rewrite the current goal using (add_SNo_0L ay2 Hay2S) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hm2ay2_le_m1m2ay2: add_SNo (mul_SNo ay ax) ay2 ≤ add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2).
We prove the intermediate claim H0le_m1: 0 ≤ mul_SNo ax ay.
An exact proof term for the current goal is Hm1NN.
We prove the intermediate claim Htmp: add_SNo 0 (add_SNo (mul_SNo ay ax) ay2) ≤ add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2).
An exact proof term for the current goal is (add_SNo_Le1 0 (add_SNo (mul_SNo ay ax) ay2) (mul_SNo ax ay) SNo_0 (SNo_add_SNo (mul_SNo ay ax) ay2 Hm2S Hay2S) Hm1S H0le_m1).
rewrite the current goal using (add_SNo_0L (add_SNo (mul_SNo ay ax) ay2) (SNo_add_SNo (mul_SNo ay ax) ay2 Hm2S Hay2S)) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hay2_le_tail: ay2 ≤ add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2).
An exact proof term for the current goal is (SNoLe_tra ay2 (add_SNo (mul_SNo ay ax) ay2) (add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2)) Hay2S (SNo_add_SNo (mul_SNo ay ax) ay2 Hm2S Hay2S) (SNo_add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2) Hm1S (SNo_add_SNo (mul_SNo ay ax) ay2 Hm2S Hay2S)) Hay2_le_m2ay2 Hm2ay2_le_m1m2ay2).
We prove the intermediate claim Hd2Le_s2: d2 ≤ s2.
rewrite the current goal using Hd2Eq (from left to right).
rewrite the current goal using Hs2Eq (from left to right).
An exact proof term for the current goal is (add_SNo_Le2 ax2 ay2 (add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2)) Hax2S Hay2S (SNo_add_SNo (mul_SNo ax ay) (add_SNo (mul_SNo ay ax) ay2) Hm1S (SNo_add_SNo (mul_SNo ay ax) ay2 Hm2S Hay2S)) Hay2_le_tail).
Apply (SNo_nonneg_sqr_Le_imp_Le d s HdS HsS HdNN HsNN) to the current goal.
We prove the intermediate claim Hd2Def: d2 = mul_SNo d d.
Use reflexivity.
We prove the intermediate claim Hs2Def: s2 = mul_SNo s s.
Use reflexivity.
rewrite the current goal using Hd2Def (from right to left).
rewrite the current goal using Hs2Def (from right to left).
An exact proof term for the current goal is Hd2Le_s2.
∎