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 Rle t 0.
Apply (ReplE_impred A (λa0 : set ⇒ minus_SNo (apply_fun d (x,a0))) t Ht (Rle t 0)) 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).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun d (x,a)) 0).
An exact proof term for the current goal is (metric_on_nonneg X d x a Hm HxX HaX).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is (Rle_minus_nonneg (apply_fun d (x,a)) HdR Hnlt).
∎