Let X, d, x, y and z be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

Assume Hz: z ∈ X.

Apply Hm to the current goal.

Assume Hcore Htri.

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

∎