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 a to be the term abs_SNo dx.
Set d to be the term distance_R2 p 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 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 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 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 HdxS: SNo dx.
An exact proof term for the current goal is (real_SNo dx HdxR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (SNo_abs_SNo dx HdxS).
We prove the intermediate claim Ha0le: 0 ≤ a.
An exact proof term for the current goal is (abs_SNo_nonneg dx HdxS).
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 Hd0le: 0 ≤ d.
An exact proof term for the current goal is (distance_R2_nonneg p c Hp Hc).
We prove the intermediate claim Hsqle: mul_SNo a a ≤ mul_SNo d d.
An exact proof term for the current goal is (abs_dx2_le_distance_R2_sqr p c Hp Hc).
Apply (SNoLtLe_or d a HdS HaS) to the current goal.
Assume Hlt: d < a.
We prove the intermediate claim Hsqrlt: mul_SNo d d < mul_SNo a a.
An exact proof term for the current goal is (SNo_sqr_lt_of_lt_nonneg d a HdS HaS Hd0le Hlt).
We prove the intermediate claim Hd2S: SNo (mul_SNo d d).
An exact proof term for the current goal is (SNo_mul_SNo d d HdS HdS).
We prove the intermediate claim Ha2S: SNo (mul_SNo a a).
An exact proof term for the current goal is (SNo_mul_SNo a a HaS HaS).
We prove the intermediate claim Hbad: mul_SNo d d < mul_SNo d d.
An exact proof term for the current goal is (SNoLtLe_tra (mul_SNo d d) (mul_SNo a a) (mul_SNo d d) Hd2S Ha2S Hd2S Hsqrlt Hsqle).
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo d d)) Hbad) (a ≤ d)).
Assume Hle: a ≤ d.
An exact proof term for the current goal is Hle.
∎