Let X, d, x, n, y and z be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HnO: n ∈ ω.
Assume Hy: y ∈ open_ball X d x (eps_ (ordsucc n)).
Assume Hz: z ∈ open_ball X d x (eps_ (ordsucc n)).
We prove the intermediate claim Hlt2: Rlt (apply_fun d (y,z)) (add_SNo (eps_ (ordsucc n)) (eps_ (ordsucc n))).
An exact proof term for the current goal is (open_ball_pair_dist_lt_add_radius X d x (eps_ (ordsucc n)) y z Hm HxX Hy Hz).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim Heq: add_SNo (eps_ (ordsucc n)) (eps_ (ordsucc n)) = eps_ n.
An exact proof term for the current goal is (eps_ordsucc_half_add n HnNat).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hlt2.
∎