Let X, d, x and A be given.

Assume Hm: metric_on X d.

Assume HxX: x ∈ X.

Assume HAsub: A ⊆ X.

Assume HAne: A ≠ Empty.

Set l to be the term metric_sup_neg_dists X d x A.

We prove the intermediate claim Hlub: R_lub (metric_neg_dists X d x A) l.

An exact proof term for the current goal is (metric_sup_neg_dists_is_lub X d x A Hm HxX HAsub HAne).

We prove the intermediate claim HlR: l ∈ R.

An exact proof term for the current goal is (R_lub_in_R (metric_neg_dists X d x A) l Hlub).

We will prove metric_dist_to_set X d x A ∈ R.

We prove the intermediate claim Hdef: metric_dist_to_set X d x A = minus_SNo l.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

An exact proof term for the current goal is (real_minus_SNo l HlR).

∎