Apply andI to the current goal.

Let pq be given.

Assume Hpq: pq ∈ (setprod EuclidPlane EuclidPlane).

We will prove apply_fun EuclidPlane_metric pq ∈ R.

rewrite the current goal using (apply_fun_graph (setprod EuclidPlane EuclidPlane) (λpq0 : set ⇒ distance_R2 (pq0 0) (pq0 1)) pq Hpq) (from left to right).

We prove the intermediate claim Hp: (pq 0) ∈ EuclidPlane.

An exact proof term for the current goal is (ap0_Sigma EuclidPlane (λ_ : set ⇒ EuclidPlane) pq Hpq).

We prove the intermediate claim Hq: (pq 1) ∈ EuclidPlane.

An exact proof term for the current goal is (ap1_Sigma EuclidPlane (λ_ : set ⇒ EuclidPlane) pq Hpq).

An exact proof term for the current goal is (distance_R2_in_R (pq 0) (pq 1) Hp Hq).

Let x and y be given.

Assume Hx: x ∈ EuclidPlane.

Assume Hy: y ∈ EuclidPlane.

rewrite the current goal using (EuclidPlane_metric_apply x y Hx Hy) (from left to right).

rewrite the current goal using (EuclidPlane_metric_apply y x Hy Hx) (from left to right).

An exact proof term for the current goal is (distance_R2_sym x y Hx Hy).

Let x be given.

Assume Hx: x ∈ EuclidPlane.

rewrite the current goal using (EuclidPlane_metric_apply x x Hx Hx) (from left to right).

An exact proof term for the current goal is (distance_R2_refl_0 x Hx).

Let x and y be given.

Assume Hx: x ∈ EuclidPlane.

Assume Hy: y ∈ EuclidPlane.

We will prove ¬ (Rlt (apply_fun EuclidPlane_metric (x,y)) 0) ∧ (apply_fun EuclidPlane_metric (x,y) = 0 → x = y).

Apply andI to the current goal.

We will prove ¬ (Rlt (apply_fun EuclidPlane_metric (x,y)) 0).

Assume Hlt: Rlt (apply_fun EuclidPlane_metric (x,y)) 0.

We will prove False.

We prove the intermediate claim Hlt2: Rlt (distance_R2 x y) 0.

rewrite the current goal using (EuclidPlane_metric_apply x y Hx Hy) (from right to left).

An exact proof term for the current goal is Hlt.

We prove the intermediate claim HdR: distance_R2 x y ∈ R.

An exact proof term for the current goal is (distance_R2_in_R x y Hx Hy).

We prove the intermediate claim HdS: SNo (distance_R2 x y).

An exact proof term for the current goal is (real_SNo (distance_R2 x y) HdR).

We prove the intermediate claim Hdlt0: (distance_R2 x y) < 0.

An exact proof term for the current goal is (RltE_lt (distance_R2 x y) 0 Hlt2).

We prove the intermediate claim Hdle0: (distance_R2 x y) ≤ 0.

An exact proof term for the current goal is (SNoLtLe (distance_R2 x y) 0 Hdlt0).

We prove the intermediate claim H0led: 0 ≤ distance_R2 x y.

An exact proof term for the current goal is (distance_R2_nonneg x y Hx Hy).

We prove the intermediate claim Hdeq0: distance_R2 x y = 0.

An exact proof term for the current goal is (SNoLe_antisym (distance_R2 x y) 0 HdS SNo_0 Hdle0 H0led).

We prove the intermediate claim Hbad: 0 < 0.

rewrite the current goal using Hdeq0 (from right to left) at position 1.

An exact proof term for the current goal is Hdlt0.

An exact proof term for the current goal is ((SNoLt_irref 0) Hbad).

Assume Hd0: apply_fun EuclidPlane_metric (x,y) = 0.

We prove the intermediate claim Hd02: distance_R2 x y = 0.

rewrite the current goal using (EuclidPlane_metric_apply x y Hx Hy) (from right to left).

An exact proof term for the current goal is Hd0.

An exact proof term for the current goal is (distance_R2_eq0 x y Hx Hy Hd02).

Let x, y and z be given.

Assume Hx: x ∈ EuclidPlane.

Assume Hy: y ∈ EuclidPlane.

Assume Hz: z ∈ EuclidPlane.

We will prove ¬ (Rlt (add_SNo (apply_fun EuclidPlane_metric (x,y)) (apply_fun EuclidPlane_metric (y,z))) (apply_fun EuclidPlane_metric (x,z))).

rewrite the current goal using (EuclidPlane_metric_apply x y Hx Hy) (from left to right).

rewrite the current goal using (EuclidPlane_metric_apply y z Hy Hz) (from left to right).

rewrite the current goal using (EuclidPlane_metric_apply x z Hx Hz) (from left to right).

We prove the intermediate claim Htri: Rle (distance_R2 x z) (add_SNo (distance_R2 x y) (distance_R2 y z)).

An exact proof term for the current goal is (distance_R2_triangle_Rle x y z Hx Hy Hz).

An exact proof term for the current goal is (RleE_nlt (distance_R2 x z) (add_SNo (distance_R2 x y) (distance_R2 y z)) Htri).