Let X, d, x and y be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

We prove the intermediate claim Hpos: ∀x0 y0 : set, x0 ∈ X → y0 ∈ X → ¬ (Rlt (apply_fun d (x0,y0)) 0) ∧ (apply_fun d (x0,y0) = 0 → x0 = y0).

Apply Hm to the current goal.

Assume Hcore Htri.

Apply Hcore to the current goal.

Assume Hcore2 Hposdef.

An exact proof term for the current goal is Hposdef.

An exact proof term for the current goal is (andEL (¬ (Rlt (apply_fun d (x,y)) 0)) (apply_fun d (x,y) = 0 → x = y) (Hpos x y Hx Hy)).

∎