linarith [h.dist, h'.dist, dist_triangle u v w]
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ u v w x : V
h : sbtw u v x
h' : sbtw v w x
this : u ≠ w
⊢ Dist.dist u w + Dist.dist w x ≤ Dist.dist u x
no goals