Let p and c be given.
Assume Hp Hc.
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.
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 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 HmxpR: minus_SNo xp ∈ R.
An exact proof term for the current goal is (real_minus_SNo xp HxpR).
We prove the intermediate claim HmypR: minus_SNo yp ∈ R.
An exact proof term for the current goal is (real_minus_SNo yp HypR).
We prove the intermediate claim HmxcR: minus_SNo xc ∈ R.
An exact proof term for the current goal is (real_minus_SNo xc HxcR).
We prove the intermediate claim HmycR: minus_SNo yc ∈ R.
An exact proof term for the current goal is (real_minus_SNo yc HycR).
We prove the intermediate claim HmxpS: SNo (minus_SNo xp).
An exact proof term for the current goal is (real_SNo (minus_SNo xp) HmxpR).
We prove the intermediate claim HmypS: SNo (minus_SNo yp).
An exact proof term for the current goal is (real_SNo (minus_SNo yp) HmypR).
We prove the intermediate claim HmxcS: SNo (minus_SNo xc).
An exact proof term for the current goal is (real_SNo (minus_SNo xc) HmxcR).
We prove the intermediate claim HmycS: SNo (minus_SNo yc).
An exact proof term for the current goal is (real_SNo (minus_SNo yc) HmycR).
We prove the intermediate claim Hswapx: add_SNo xc (minus_SNo xp) = minus_SNo (add_SNo xp (minus_SNo xc)).
We prove the intermediate claim Hneg: minus_SNo (add_SNo xp (minus_SNo xc)) = add_SNo (minus_SNo xp) (minus_SNo (minus_SNo xc)).
An exact proof term for the current goal is (minus_add_SNo_distr xp (minus_SNo xc) HxpS HmxcS).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo xc) = xc.
An exact proof term for the current goal is (minus_SNo_invol xc HxcS).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo xp (minus_SNo xc)) = add_SNo (minus_SNo xp) xc.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo xp) xc = add_SNo xc (minus_SNo xp).
An exact proof term for the current goal is (add_SNo_com (minus_SNo xp) xc HmxpS HxcS).
We will prove add_SNo xc (minus_SNo xp) = minus_SNo (add_SNo xp (minus_SNo xc)).
rewrite the current goal using Hcom (from right to left).
rewrite the current goal using Hneg2 (from right to left).
Use reflexivity.
We prove the intermediate claim Hswapy: add_SNo yc (minus_SNo yp) = minus_SNo (add_SNo yp (minus_SNo yc)).
We prove the intermediate claim Hneg: minus_SNo (add_SNo yp (minus_SNo yc)) = add_SNo (minus_SNo yp) (minus_SNo (minus_SNo yc)).
An exact proof term for the current goal is (minus_add_SNo_distr yp (minus_SNo yc) HypS HmycS).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo yc) = yc.
An exact proof term for the current goal is (minus_SNo_invol yc HycS).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo yp (minus_SNo yc)) = add_SNo (minus_SNo yp) yc.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo yp) yc = add_SNo yc (minus_SNo yp).
An exact proof term for the current goal is (add_SNo_com (minus_SNo yp) yc HmypS HycS).
We will prove add_SNo yc (minus_SNo yp) = minus_SNo (add_SNo yp (minus_SNo yc)).
rewrite the current goal using Hcom (from right to left).
rewrite the current goal using Hneg2 (from right to left).
Use reflexivity.
We prove the intermediate claim HdxR: add_SNo xp (minus_SNo xc) ∈ R.
An exact proof term for the current goal is (real_add_SNo xp HxpR (minus_SNo xc) HmxcR).
We prove the intermediate claim HdyR: add_SNo yp (minus_SNo yc) ∈ R.
An exact proof term for the current goal is (real_add_SNo yp HypR (minus_SNo yc) HmycR).
We prove the intermediate claim HdxS: SNo (add_SNo xp (minus_SNo xc)).
An exact proof term for the current goal is (real_SNo (add_SNo xp (minus_SNo xc)) HdxR).
We prove the intermediate claim HdyS: SNo (add_SNo yp (minus_SNo yc)).
An exact proof term for the current goal is (real_SNo (add_SNo yp (minus_SNo yc)) HdyR).
We prove the intermediate claim Hsqx: mul_SNo (add_SNo xc (minus_SNo xp)) (add_SNo xc (minus_SNo xp)) = mul_SNo (add_SNo xp (minus_SNo xc)) (add_SNo xp (minus_SNo xc)).
rewrite the current goal using Hswapx (from left to right).
rewrite the current goal using (mul_SNo_minus_minus (add_SNo xp (minus_SNo xc)) (add_SNo xp (minus_SNo xc)) HdxS HdxS) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsqy: mul_SNo (add_SNo yc (minus_SNo yp)) (add_SNo yc (minus_SNo yp)) = mul_SNo (add_SNo yp (minus_SNo yc)) (add_SNo yp (minus_SNo yc)).
rewrite the current goal using Hswapy (from left to right).
rewrite the current goal using (mul_SNo_minus_minus (add_SNo yp (minus_SNo yc)) (add_SNo yp (minus_SNo yc)) HdyS HdyS) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdefpc: distance_R2 p c = sqrt_SNo_nonneg (add_SNo (mul_SNo (add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord c))) (add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord c)))) (mul_SNo (add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord c))) (add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord c))))).
Use reflexivity.
We prove the intermediate claim Hdefcp: distance_R2 c p = sqrt_SNo_nonneg (add_SNo (mul_SNo (add_SNo (R2_xcoord c) (minus_SNo (R2_xcoord p))) (add_SNo (R2_xcoord c) (minus_SNo (R2_xcoord p)))) (mul_SNo (add_SNo (R2_ycoord c) (minus_SNo (R2_ycoord p))) (add_SNo (R2_ycoord c) (minus_SNo (R2_ycoord p))))).
Use reflexivity.
rewrite the current goal using Hdefpc (from left to right).
rewrite the current goal using Hdefcp (from left to right).
rewrite the current goal using Hsqx (from left to right).
rewrite the current goal using Hsqy (from left to right).
Use reflexivity.
∎