Let X, d, x, y, p, r1 and r2 be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HpX: p ∈ X.
Assume Hr1R: r1 ∈ R.
Assume Hr2R: r2 ∈ R.
Assume HpB1: p ∈ open_ball X d x r1.
Assume HpB2: p ∈ open_ball X d y r2.
We prove the intermediate claim Hdxp: Rlt (apply_fun d (x,p)) r1.
An exact proof term for the current goal is (open_ballE2 X d x r1 p HpB1).
We prove the intermediate claim Hdyp: Rlt (apply_fun d (y,p)) r2.
An exact proof term for the current goal is (open_ballE2 X d y r2 p HpB2).
We prove the intermediate claim Hdpy: Rlt (apply_fun d (p,y)) r2.
rewrite the current goal using (metric_on_symmetric X d y p Hm HyX HpX) (from right to left).
An exact proof term for the current goal is Hdyp.
We prove the intermediate claim Htri: Rle (apply_fun d (x,y)) (add_SNo (apply_fun d (x,p)) (apply_fun d (p,y))).
An exact proof term for the current goal is (metric_triangle_Rle X d x p y Hm HxX HpX HyX).
We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun d (x,p)) (apply_fun d (p,y))) (add_SNo r1 r2).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun d (x,p)) r1 (apply_fun d (p,y)) r2 Hdxp Hdpy).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (x,y)) (add_SNo (apply_fun d (x,p)) (apply_fun d (p,y))) (add_SNo r1 r2) Htri HsumLt).
∎