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 S to be the term metric_neg_dists X d x A.
We prove the intermediate claim HexS: ∃t0 : set, t0 ∈ S.
We prove the intermediate claim HexA: ∃a0 : set, a0 ∈ A.
An exact proof term for the current goal is (nonempty_has_element A HAne).
Set a0 to be the term Eps_i (λa : set ⇒ a ∈ A).
We prove the intermediate claim Ha0: a0 ∈ A.
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ A) HexA).
We use (minus_SNo (apply_fun d (x,a0))) to witness the existential quantifier.
We will prove minus_SNo (apply_fun d (x,a0)) ∈ S.
We prove the intermediate claim HSdef: S = metric_neg_dists X d x A.
Use reflexivity.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (ReplI A (λa : set ⇒ minus_SNo (apply_fun d (x,a))) a0 Ha0).
We prove the intermediate claim HS_R: ∀t : set, t ∈ S → t ∈ R.
Let t be given.
Assume HtS: t ∈ S.
An exact proof term for the current goal is (metric_neg_dists_in_R X d x A Hm HxX HAsub t HtS).
We prove the intermediate claim HubS: ∃u : set, u ∈ R ∧ ∀t : set, t ∈ S → t ∈ R → Rle t u.
We use 0 to witness the existential quantifier.
We will prove 0 ∈ R ∧ ∀t : set, t ∈ S → t ∈ R → Rle t 0.
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).
We prove the intermediate claim Hexlub: ∃l : set, R_lub S l.
An exact proof term for the current goal is (R_lub_exists S HexS HS_R HubS).
An exact proof term for the current goal is (Eps_i_ex (λl : set ⇒ R_lub S l) Hexlub).
∎