no goals
α : Type u_1
β : Type ?u.576655
ι : Type ?u.576658
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C r : ℝ
hr : r < 1
u : ℕ → α
h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ C * r ^ n
simpa [dist_eq_norm] using h