Let X, d, S, n, p, x and y be given.
Assume Hm: metric_on X d.
Assume HnO: n ∈ ω.
Assume Hsep: eps_separated_set X d S n.
Assume HpX: p ∈ X.
Assume HxS: x ∈ S.
Assume HyS: y ∈ S.
Assume HpBx: p ∈ open_ball X d x (eps_ (ordsucc n)).
Assume HpBy: p ∈ open_ball X d y (eps_ (ordsucc n)).
Apply (xm (x = y)) to the current goal.
Assume Hxy: x = y.
An exact proof term for the current goal is Hxy.
Assume HxyNe: ¬ (x = y).
We prove the intermediate claim HSsubX: S ⊆ X.
An exact proof term for the current goal is (andEL (S ⊆ X) (∀x0 y0 : set, x0 ∈ S → y0 ∈ S → ¬ (x0 = y0) → ¬ (Rlt (apply_fun d (x0,y0)) (eps_ n))) Hsep).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HSsubX x HxS).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HSsubX y HyS).
We prove the intermediate claim HpX1: p ∈ X.
An exact proof term for the current goal is HpX.
We prove the intermediate claim HepsR: eps_ (ordsucc n) ∈ R.
An exact proof term for the current goal is (RltE_right (apply_fun d (x,p)) (eps_ (ordsucc n)) (open_ballE2 X d x (eps_ (ordsucc n)) p HpBx)).
We prove the intermediate claim HdxyLtSum: Rlt (apply_fun d (x,y)) (add_SNo (eps_ (ordsucc n)) (eps_ (ordsucc n))).
An exact proof term for the current goal is (metric_ball_intersect_centers_lt_add X d x y p (eps_ (ordsucc n)) (eps_ (ordsucc n)) Hm HxX HyX HpX1 HepsR HepsR HpBx HpBy).
We prove the intermediate claim Hnat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HdxyLtEps: Rlt (apply_fun d (x,y)) (eps_ n).
rewrite the current goal using (eps_ordsucc_half_add n Hnat) (from right to left).
An exact proof term for the current goal is HdxyLtSum.
We prove the intermediate claim HsepProp: ∀x0 y0 : set, x0 ∈ S → y0 ∈ S → ¬ (x0 = y0) → ¬ (Rlt (apply_fun d (x0,y0)) (eps_ n)).
An exact proof term for the current goal is (andER (S ⊆ X) (∀x0 y0 : set, x0 ∈ S → y0 ∈ S → ¬ (x0 = y0) → ¬ (Rlt (apply_fun d (x0,y0)) (eps_ n))) Hsep).
We prove the intermediate claim Hcontra: False.
An exact proof term for the current goal is ((HsepProp x y HxS HyS HxyNe) HdxyLtEps).
An exact proof term for the current goal is (FalseE Hcontra (x = y)).
∎