have := length_mul_le_pathLength_add hr.le hr' hl
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ l.length ≤ ⌊R / r + 1⌋₊