exact add_le_add (h _ _ h'.1) (length_mul_le_pathLength_add hr h h'.2)
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ r + ↑(y :: xs).length * r ≤ dist x y + ((y :: xs).pathLength + r)
no goals