Let p and c be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hc: c ∈ EuclidPlane.
Set dy to be the term add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord c)).
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 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 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 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 HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
rewrite the current goal using (abs_SNo_sqr_eq dy HdyS) (from left to right).
An exact proof term for the current goal is (dy2_le_distance_R2_sqr p c Hp Hc).
∎