no goals
α : Type u_1
β : Type ?u.1068136
ι : Type ?u.1068139
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
r : ℝ
hr : r < 1
h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (∑ k in Finset.range n, u k) (∑ k in Finset.range (n + 1), u k) ≤ C * r ^ n
simp [h]