Let X, d, x, A and a be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HAsub: A ⊆ X.
Assume HAne: A ≠ Empty.
Assume HaA: a ∈ 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 HdxaR: apply_fun d (x,a) ∈ R.
An exact proof term for the current goal is (Hfun (x,a) HxaIn).
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 prove the intermediate claim HdistDef: metric_dist_to_set X d x A = minus_SNo l.
Use reflexivity.
We prove the intermediate claim HdistR: metric_dist_to_set X d x A ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x A Hm HxX HAsub HAne).
Set t to be the term minus_SNo (apply_fun d (x,a)).
We prove the intermediate claim HtIn: t ∈ metric_neg_dists X d x A.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ minus_SNo (apply_fun d (x,a0))) a HaA).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (metric_neg_dists_in_R X d x A Hm HxX HAsub t HtIn).
We prove the intermediate claim Hcore: l ∈ R ∧ ∀s : set, s ∈ metric_neg_dists X d x A → s ∈ R → Rle s l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀s : set, s ∈ metric_neg_dists X d x A → s ∈ R → Rle s l) (∀v : set, v ∈ R → (∀s : set, s ∈ metric_neg_dists X d x A → s ∈ R → Rle s v) → Rle l v) Hlub).
We prove the intermediate claim Hub: ∀s : set, s ∈ metric_neg_dists X d x A → s ∈ R → Rle s l.
An exact proof term for the current goal is (andER (l ∈ R) (∀s : set, s ∈ metric_neg_dists X d x A → s ∈ R → Rle s l) Hcore).
We prove the intermediate claim Htle: Rle t l.
An exact proof term for the current goal is (Hub t HtIn HtR).
We prove the intermediate claim Hnlt: ¬ (Rlt l t).
An exact proof term for the current goal is (RleE_nlt t l Htle).
Apply (RleI (metric_dist_to_set X d x A) (apply_fun d (x,a)) HdistR HdxaR) to the current goal.
Assume Hlt: Rlt (apply_fun d (x,a)) (metric_dist_to_set X d x A).
We prove the intermediate claim HltS: apply_fun d (x,a) < metric_dist_to_set X d x A.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x,a)) (metric_dist_to_set X d x A) Hlt).
We prove the intermediate claim HdxaS: SNo (apply_fun d (x,a)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,a)) HdxaR).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR).
We prove the intermediate claim HdistS: SNo (metric_dist_to_set X d x A).
An exact proof term for the current goal is (real_SNo (metric_dist_to_set X d x A) HdistR).
We prove the intermediate claim HltS2: apply_fun d (x,a) < minus_SNo l.
rewrite the current goal using HdistDef (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim Hltneg: l < minus_SNo (apply_fun d (x,a)).
An exact proof term for the current goal is (minus_SNo_Lt_contra2 (apply_fun d (x,a)) l HdxaS HlS HltS2).
We prove the intermediate claim HltR2: Rlt l t.
We prove the intermediate claim HtDef: t = minus_SNo (apply_fun d (x,a)).
Use reflexivity.
rewrite the current goal using HtDef (from left to right).
An exact proof term for the current goal is (RltI l (minus_SNo (apply_fun d (x,a))) HlR (real_minus_SNo (apply_fun d (x,a)) HdxaR) Hltneg).
An exact proof term for the current goal is (Hnlt HltR2).
∎