Let X, d, x and A be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HAsub: A ⊆ X.
Assume HxA: x ∈ A.
We prove the intermediate claim HAne: A ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A x HxA).
Set S to be the term metric_neg_dists X d x A.
Set l to be the term metric_sup_neg_dists X d x A.
We prove the intermediate claim Hlub: R_lub S 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 H0inS: 0 ∈ S.
We prove the intermediate claim HxIn: minus_SNo (apply_fun d (x,x)) ∈ S.
An exact proof term for the current goal is (ReplI A (λa : set ⇒ minus_SNo (apply_fun d (x,a))) x HxA).
We prove the intermediate claim Hdxx0: apply_fun d (x,x) = 0.
An exact proof term for the current goal is (metric_on_diag_zero X d x Hm HxX).
We prove the intermediate claim H0eq: minus_SNo (apply_fun d (x,x)) = 0.
rewrite the current goal using Hdxx0 (from left to right).
An exact proof term for the current goal is minus_SNo_0.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is HxIn.
We prove the intermediate claim Hlub0: R_lub S 0.
We will prove (0 ∈ R ∧ (∀t : set, t ∈ S → t ∈ R → Rle t 0) ∧ (∀u : set, u ∈ R → (∀t : set, t ∈ S → t ∈ R → Rle t u) → Rle 0 u)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
Let t be given.
Assume HtS: t ∈ S.
Assume _: t ∈ R.
An exact proof term for the current goal is (metric_neg_dists_le_0 X d x A Hm HxX HAsub t HtS).
Let u be given.
Assume HuR: u ∈ R.
Assume Hub: ∀t : set, t ∈ S → t ∈ R → Rle t u.
An exact proof term for the current goal is (Hub 0 H0inS real_0).
We prove the intermediate claim HlEq0: l = 0.
An exact proof term for the current goal is (R_lub_unique S l 0 Hlub Hlub0).
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).
rewrite the current goal using HlEq0 (from left to right).
An exact proof term for the current goal is minus_SNo_0.
∎