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)).
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).
rewrite the current goal using (abs_SNo_sqr_eq dx HdxS) (from left to right).
An exact proof term for the current goal is (dx2_le_distance_R2_sqr p c Hp Hc).
∎