Let p and c be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hc: c ∈ EuclidPlane.
Assume Hd0: distance_R2 p c = 0.
Set xp to be the term R2_xcoord p.
Set yp to be the term R2_ycoord p.
Set xc to be the term R2_xcoord c.
Set yc to be the term R2_ycoord c.
Set dx to be the term add_SNo xp (minus_SNo xc).
Set dy to be the term add_SNo yp (minus_SNo yc).
Set dx2 to be the term mul_SNo dx dx.
Set dy2 to be the term mul_SNo dy dy.
Set sum to be the term add_SNo dx2 dy2.
We prove the intermediate claim HxpR: xp ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R p Hp).
We prove the intermediate claim HypR: yp ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R p Hp).
We prove the intermediate claim HxcR: xc ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R c Hc).
We prove the intermediate claim HycR: yc ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R c Hc).
We prove the intermediate claim HmxR: minus_SNo xc ∈ R.
An exact proof term for the current goal is (real_minus_SNo xc HxcR).
We prove the intermediate claim HmyR: minus_SNo yc ∈ R.
An exact proof term for the current goal is (real_minus_SNo yc HycR).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (real_add_SNo xp HxpR (minus_SNo xc) HmxR).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (real_add_SNo yp HypR (minus_SNo yc) HmyR).
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 (SNo_mul_SNo dx dx HdxS HdxS).
We prove the intermediate claim Hdy2S: SNo dy2.
An exact proof term for the current goal is (SNo_mul_SNo dy dy HdyS HdyS).
We prove the intermediate claim HsumS: SNo sum.
An exact proof term for the current goal is (SNo_add_SNo dx2 dy2 Hdx2S Hdy2S).
We prove the intermediate claim Hd2eq0: mul_SNo (distance_R2 p c) (distance_R2 p c) = 0.
rewrite the current goal using Hd0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsqr: mul_SNo (distance_R2 p c) (distance_R2 p c) = sum.
We will prove mul_SNo (distance_R2 p c) (distance_R2 p c) = sum.
rewrite the current goal using (distance_R2_sqr p c Hp Hc) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsum0: sum = 0.
rewrite the current goal using Hsqr (from right to left).
An exact proof term for the current goal is Hd2eq0.
We prove the intermediate claim Hdx2nonneg: 0 ≤ dx2.
An exact proof term for the current goal is (SNo_sqr_nonneg dx HdxS).
We prove the intermediate claim Hdy2nonneg: 0 ≤ dy2.
An exact proof term for the current goal is (SNo_sqr_nonneg dy HdyS).
We prove the intermediate claim Hdx2_le_sum: dx2 ≤ sum.
An exact proof term for the current goal is (SNoLe_add_nonneg_right dx2 dy2 Hdx2S Hdy2S Hdy2nonneg).
We prove the intermediate claim Hdy2_le_sum: dy2 ≤ sum.
rewrite the current goal using (add_SNo_com dx2 dy2 Hdx2S Hdy2S) (from left to right).
An exact proof term for the current goal is (SNoLe_add_nonneg_right dy2 dx2 Hdy2S Hdx2S Hdx2nonneg).
We prove the intermediate claim Hdx2le0: dx2 ≤ 0.
We will prove dx2 ≤ 0.
rewrite the current goal using Hsum0 (from right to left) at position 1.
An exact proof term for the current goal is Hdx2_le_sum.
We prove the intermediate claim Hdy2le0: dy2 ≤ 0.
We will prove dy2 ≤ 0.
rewrite the current goal using Hsum0 (from right to left) at position 1.
An exact proof term for the current goal is Hdy2_le_sum.
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim Hdx2eq0: dx2 = 0.
An exact proof term for the current goal is (SNoLe_antisym dx2 0 Hdx2S H0S Hdx2le0 Hdx2nonneg).
We prove the intermediate claim Hdy2eq0: dy2 = 0.
An exact proof term for the current goal is (SNoLe_antisym dy2 0 Hdy2S H0S Hdy2le0 Hdy2nonneg).
We prove the intermediate claim Hdx0: dx = 0.
We prove the intermediate claim Hcases: dx = 0 ∨ 0 < mul_SNo dx dx.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos dx HdxS).
Apply Hcases to the current goal.
Assume H0: dx = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo dx dx.
We prove the intermediate claim Hbad: mul_SNo dx dx < mul_SNo dx dx.
We prove the intermediate claim Hdx2def: dx2 = mul_SNo dx dx.
Use reflexivity.
We prove the intermediate claim Hdx2zero: mul_SNo dx dx = 0.
rewrite the current goal using Hdx2def (from right to left) at position 1.
An exact proof term for the current goal is Hdx2eq0.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hdx2zero (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
rewrite the current goal using Hdx2zero (from left to right) at position 2.
rewrite the current goal using Hdx2zero (from left to right) at position 1.
An exact proof term for the current goal is Hpos0.
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo dx dx)) Hbad) (dx = 0)).
We prove the intermediate claim Hdy0: dy = 0.
We prove the intermediate claim Hcases: dy = 0 ∨ 0 < mul_SNo dy dy.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos dy HdyS).
Apply Hcases to the current goal.
Assume H0: dy = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo dy dy.
We prove the intermediate claim Hbad: mul_SNo dy dy < mul_SNo dy dy.
We prove the intermediate claim Hdy2def: dy2 = mul_SNo dy dy.
Use reflexivity.
We prove the intermediate claim Hdy2zero: mul_SNo dy dy = 0.
rewrite the current goal using Hdy2def (from right to left) at position 1.
An exact proof term for the current goal is Hdy2eq0.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hdy2zero (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
rewrite the current goal using Hdy2zero (from left to right) at position 2.
rewrite the current goal using Hdy2zero (from left to right) at position 1.
An exact proof term for the current goal is Hpos0.
An exact proof term for the current goal is (FalseE ((SNoLt_irref (mul_SNo dy dy)) Hbad) (dy = 0)).
We prove the intermediate claim HxpS: SNo xp.
An exact proof term for the current goal is (real_SNo xp HxpR).
We prove the intermediate claim HypS: SNo yp.
An exact proof term for the current goal is (real_SNo yp HypR).
We prove the intermediate claim HxcS: SNo xc.
An exact proof term for the current goal is (real_SNo xc HxcR).
We prove the intermediate claim HycS: SNo yc.
An exact proof term for the current goal is (real_SNo yc HycR).
We prove the intermediate claim HmxcS: SNo (minus_SNo xc).
An exact proof term for the current goal is (SNo_minus_SNo xc HxcS).
We prove the intermediate claim HmycS: SNo (minus_SNo yc).
An exact proof term for the current goal is (SNo_minus_SNo yc HycS).
We prove the intermediate claim Hxp_eq_xc: xp = xc.
We prove the intermediate claim HdxDef: dx = add_SNo xp (minus_SNo xc).
Use reflexivity.
We prove the intermediate claim Hdx0': add_SNo xp (minus_SNo xc) = 0.
rewrite the current goal using HdxDef (from right to left).
An exact proof term for the current goal is Hdx0.
We prove the intermediate claim Hl_to_xc: add_SNo (add_SNo xp (minus_SNo xc)) xc = xc.
rewrite the current goal using Hdx0' (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_0L xc HxcS).
We prove the intermediate claim Hl_to_xp: add_SNo (add_SNo xp (minus_SNo xc)) xc = xp.
rewrite the current goal using (add_SNo_assoc xp (minus_SNo xc) xc HxpS HmxcS HxcS) (from right to left).
rewrite the current goal using (add_SNo_com (minus_SNo xc) xc HmxcS HxcS) (from left to right).
rewrite the current goal using (add_SNo_assoc xp xc (minus_SNo xc) HxpS HxcS HmxcS) (from left to right).
rewrite the current goal using (add_SNo_minus_R2 xp xc HxpS HxcS) (from left to right).
Use reflexivity.
We will prove xp = xc.
rewrite the current goal using Hl_to_xp (from right to left) at position 1.
An exact proof term for the current goal is Hl_to_xc.
We prove the intermediate claim Hyp_eq_yc: yp = yc.
We prove the intermediate claim HdyDef: dy = add_SNo yp (minus_SNo yc).
Use reflexivity.
We prove the intermediate claim Hdy0': add_SNo yp (minus_SNo yc) = 0.
rewrite the current goal using HdyDef (from right to left).
An exact proof term for the current goal is Hdy0.
We prove the intermediate claim Hl_to_yc: add_SNo (add_SNo yp (minus_SNo yc)) yc = yc.
rewrite the current goal using Hdy0' (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_0L yc HycS).
We prove the intermediate claim Hl_to_yp: add_SNo (add_SNo yp (minus_SNo yc)) yc = yp.
rewrite the current goal using (add_SNo_assoc yp (minus_SNo yc) yc HypS HmycS HycS) (from right to left).
rewrite the current goal using (add_SNo_com (minus_SNo yc) yc HmycS HycS) (from left to right).
rewrite the current goal using (add_SNo_assoc yp yc (minus_SNo yc) HypS HycS HmycS) (from left to right).
rewrite the current goal using (add_SNo_minus_R2 yp yc HypS HycS) (from left to right).
Use reflexivity.
We will prove yp = yc.
rewrite the current goal using Hl_to_yp (from right to left) at position 1.
An exact proof term for the current goal is Hl_to_yc.
We prove the intermediate claim Hp_eta: (xp,yp) = p.
An exact proof term for the current goal is (EuclidPlane_eta p Hp).
We prove the intermediate claim Hc_eta: (xc,yc) = c.
An exact proof term for the current goal is (EuclidPlane_eta c Hc).
rewrite the current goal using Hp_eta (from right to left).
rewrite the current goal using Hc_eta (from right to left).
rewrite the current goal using Hxp_eq_xc (from left to right).
rewrite the current goal using Hyp_eq_yc (from left to right).
Use reflexivity.
∎