Let X, d, x and A be given.

Assume Hm: metric_on X d.

Assume HxX: x ∈ X.

Assume HAsub: A ⊆ X.

Let t be given.

Assume Ht: t ∈ metric_neg_dists X d x A.

We will prove t ∈ R.

Apply (ReplE_impred A (λa0 : set ⇒ minus_SNo (apply_fun d (x,a0))) t Ht (t ∈ R)) to the current goal.

Let a be given.

Assume HaA: a ∈ A.

Assume Hteq: t = minus_SNo (apply_fun d (x,a)).

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (HAsub a HaA).

We prove the intermediate claim Hfun: function_on d (setprod X X) R.

An exact proof term for the current goal is (metric_on_function_on X d Hm).

We prove the intermediate claim HxaIn: (x,a) ∈ setprod X X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x a HxX HaX).

We prove the intermediate claim HdR: apply_fun d (x,a) ∈ R.

An exact proof term for the current goal is (Hfun (x,a) HxaIn).

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

An exact proof term for the current goal is (real_minus_SNo (apply_fun d (x,a)) HdR).

∎