Let X, d, x and y be given.
Assume Hm: metric_on X d.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
Assume H0: apply_fun d (x,y) = 0.
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.
We prove the intermediate claim Himp: apply_fun d (x,y) = 0 → x = y.
An exact proof term for the current goal is (andER (¬ (Rlt (apply_fun d (x,y)) 0)) (apply_fun d (x,y) = 0 → x = y) (Hpos x y Hx Hy)).
An exact proof term for the current goal is (Himp H0).
∎