Let X, d, x, r, y and z be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume Hy: y ∈ open_ball X d x r.
Assume Hz: z ∈ open_ball X d x r.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r y Hy).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r z Hz).
We prove the intermediate claim Hxy: Rlt (apply_fun d (x,y)) r.
An exact proof term for the current goal is (open_ballE2 X d x r y Hy).
We prove the intermediate claim Hxz: Rlt (apply_fun d (x,z)) r.
An exact proof term for the current goal is (open_ballE2 X d x r z Hz).
We prove the intermediate claim Hsymxy: apply_fun d (x,y) = apply_fun d (y,x).
An exact proof term for the current goal is (metric_on_symmetric X d x y Hm HxX HyX).
We prove the intermediate claim Hyx: Rlt (apply_fun d (y,x)) r.
rewrite the current goal using Hsymxy (from right to left).
An exact proof term for the current goal is Hxy.
We prove the intermediate claim Hle: Rle (apply_fun d (y,z)) (add_SNo (apply_fun d (y,x)) (apply_fun d (x,z))).
An exact proof term for the current goal is (metric_triangle_Rle X d y x z Hm HyX HxX HzX).
We prove the intermediate claim Hlt: Rlt (add_SNo (apply_fun d (y,x)) (apply_fun d (x,z))) (add_SNo r r).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun d (y,x)) r (apply_fun d (x,z)) r Hyx Hxz).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (apply_fun d (y,z)) (add_SNo (apply_fun d (y,x)) (apply_fun d (x,z))) (add_SNo r r) Hle Hlt).
∎