Let p and c be given.
Assume Hp Hc.
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 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 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 Hc1R: R2_ycoord c ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R c Hc).
Set dx to be the term add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord c)).
Set dy to be the term add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord c)).
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 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 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 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).
Set dx2 to be the term mul_SNo dx dx.
Set dy2 to be the term mul_SNo dy dy.
We prove the intermediate claim Hdx2def: dx2 = mul_SNo dx dx.
Use reflexivity.
We prove the intermediate claim Hdy2def: dy2 = mul_SNo dy dy.
Use reflexivity.
We prove the intermediate claim Hdx2R: dx2 ∈ R.
An exact proof term for the current goal is (real_mul_SNo dx HdxR dx HdxR).
We prove the intermediate claim Hdy2R: dy2 ∈ R.
An exact proof term for the current goal is (real_mul_SNo dy HdyR dy HdyR).
Set sum to be the term add_SNo dx2 dy2.
We prove the intermediate claim Hsumdef: sum = add_SNo dx2 dy2.
Use reflexivity.
We prove the intermediate claim HsumR: sum ∈ R.
An exact proof term for the current goal is (real_add_SNo dx2 Hdx2R dy2 Hdy2R).
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 HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
We prove the intermediate claim Hdx2S: SNo dx2.
An exact proof term for the current goal is (real_SNo dx2 Hdx2R).
We prove the intermediate claim Hdy2S: SNo dy2.
An exact proof term for the current goal is (real_SNo dy2 Hdy2R).
We prove the intermediate claim Hdx2nonneg: 0 ≤ dx2.
We prove the intermediate claim H0or: dx = 0 ∨ 0 < (mul_SNo dx dx).
An exact proof term for the current goal is (SNo_zero_or_sqr_pos dx HdxS).
Apply H0or to the current goal.
Assume Hdx0: dx = 0.
rewrite the current goal using Hdx2def (from left to right).
rewrite the current goal using Hdx0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume Hpos: 0 < (mul_SNo dx dx).
rewrite the current goal using Hdx2def (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 (mul_SNo dx dx) Hpos).
We prove the intermediate claim Hdy2nonneg: 0 ≤ dy2.
We prove the intermediate claim H0or: dy = 0 ∨ 0 < (mul_SNo dy dy).
An exact proof term for the current goal is (SNo_zero_or_sqr_pos dy HdyS).
Apply H0or to the current goal.
Assume Hdy0: dy = 0.
rewrite the current goal using Hdy2def (from left to right).
rewrite the current goal using Hdy0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume Hpos: 0 < (mul_SNo dy dy).
rewrite the current goal using Hdy2def (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 (mul_SNo dy dy) Hpos).
We prove the intermediate claim HsumNonneg: 0 ≤ sum.
rewrite the current goal using Hsumdef (from left to right).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le3 0 0 dx2 dy2 SNo_0 SNo_0 Hdx2S Hdy2S Hdx2nonneg Hdy2nonneg).
We prove the intermediate claim Hdef: distance_R2 p c = sqrt_SNo_nonneg sum.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (sqrt_SNo_nonneg_real sum HsumR HsumNonneg).
∎