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)).
We prove the intermediate claim Hp0R: R2_xcoord p ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R p Hp).
We prove the intermediate claim Hp1R: R2_ycoord p ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R p Hp).
We prove the intermediate claim Hc0R: R2_xcoord c ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R c Hc).
We prove the intermediate claim Hc1R: R2_ycoord c ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R c Hc).
We prove the intermediate claim Hmx: minus_SNo (R2_xcoord c) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_xcoord c) Hc0R).
We prove the intermediate claim Hmy: minus_SNo (R2_ycoord c) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_ycoord c) Hc1R).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_xcoord p) Hp0R (minus_SNo (R2_xcoord c)) Hmx).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_ycoord p) Hp1R (minus_SNo (R2_ycoord c)) Hmy).
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).
Set dx2 to be the term mul_SNo dx dx.
Set dy2 to be the term mul_SNo dy dy.
We prove the intermediate claim Hdx2R: dx2 ∈ R.
An exact proof term for the current goal is (real_mul_SNo dx HdxR dx HdxR).
We prove the intermediate claim Hdy2R: dy2 ∈ R.
An exact proof term for the current goal is (real_mul_SNo dy HdyR dy HdyR).
We prove the intermediate claim Hdx2S: SNo dx2.
An exact proof term for the current goal is (real_SNo dx2 Hdx2R).
We prove the intermediate claim Hdy2S: SNo dy2.
An exact proof term for the current goal is (real_SNo dy2 Hdy2R).
We prove the intermediate claim Hdy2nonneg: 0 ≤ dy2.
An exact proof term for the current goal is (SNo_sqr_nonneg dy HdyS).
We will prove mul_SNo dx dx ≤ mul_SNo (distance_R2 p c) (distance_R2 p c).
rewrite the current goal using (distance_R2_sqr p c Hp Hc) (from left to right).
An exact proof term for the current goal is (SNoLe_add_nonneg_right dx2 dy2 Hdx2S Hdy2S Hdy2nonneg).
∎