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 dx to be the term add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord x)).
Set a to be the term abs_SNo dx.
Set d to be the term distance_R2 p x.
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 Hx0R: R2_xcoord x ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R x Hx).
We prove the intermediate claim Hmx: minus_SNo (R2_xcoord x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (R2_xcoord x) Hx0R).
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 x)) 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 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_dx_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).
∎