Let X, d and x be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

We prove the intermediate claim Hrefl: ∀x0 : set, x0 ∈ X → apply_fun d (x0,x0) = 0.

Apply Hm to the current goal.

Assume Hcore Htri.

Apply Hcore to the current goal.

Assume Hcore2 Hposdef.

Apply Hcore2 to the current goal.

Assume Hab Hrefl.

An exact proof term for the current goal is Hrefl.

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

∎