Let p, x and r be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hx: x ∈ EuclidPlane.
Assume HrR: r ∈ R.
Assume Hdr: Rlt (distance_R2 p x) r.
Set dy to be the term add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord x)).
Set a to be the term abs_SNo dy.
Set d to be the term distance_R2 p x.
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 Hx1R: R2_ycoord x ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R x Hx).
We prove the intermediate claim Hmy: minus_SNo (R2_ycoord x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_ycoord x) Hx1R).
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 x)) 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 HdR: d ∈ R.
An exact proof term for the current goal is (distance_R2_in_R p x Hp Hx).
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 HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim Hle: a ≤ d.
An exact proof term for the current goal is (abs_dy_le_distance_R2 p x Hp Hx).
We prove the intermediate claim Hdlt: d < r.
An exact proof term for the current goal is (RltE_lt d r Hdr).
An exact proof term for the current goal is (SNoLeLt_tra a d r HaS HdS HrS Hle Hdlt).
∎