Let X and d be given.

Assume Hm: metric_on X d.

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.

Apply Hab to the current goal.

Assume Hf Hsym.

An exact proof term for the current goal is Hf.

∎