Let p be given.

Assume Hp.

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 Hp0S: SNo (R2_xcoord p).

An exact proof term for the current goal is (real_SNo (R2_xcoord p) Hp0R).

We prove the intermediate claim Hp1S: SNo (R2_ycoord p).

An exact proof term for the current goal is (real_SNo (R2_ycoord p) Hp1R).

We prove the intermediate claim Hdx: add_SNo (R2_xcoord p) (minus_SNo (R2_xcoord p)) = 0.

An exact proof term for the current goal is (add_SNo_minus_SNo_rinv (R2_xcoord p) Hp0S).

We prove the intermediate claim Hdy: add_SNo (R2_ycoord p) (minus_SNo (R2_ycoord p)) = 0.

An exact proof term for the current goal is (add_SNo_minus_SNo_rinv (R2_ycoord p) Hp1S).

rewrite the current goal using Hdx (from left to right).

An exact proof term for the current goal is (mul_SNo_zeroR 0 SNo_0).

rewrite the current goal using Hdy (from left to right).

An exact proof term for the current goal is (mul_SNo_zeroR 0 SNo_0).

rewrite the current goal using Hdx2 (from left to right).

rewrite the current goal using Hdy2 (from left to right).

An exact proof term for the current goal is (add_SNo_0L 0 SNo_0).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using Hsum (from left to right).

rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).

Use reflexivity.

∎