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)).
Set a to be the term abs_SNo dy.
Set d to be the term distance_R2 p 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).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (SNo_abs_SNo dy HdyS).
We prove the intermediate claim Ha0le: 0 ≤ a.
An exact proof term for the current goal is (abs_SNo_nonneg 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 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_dy2_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.
∎