no goals
α : Type u_1
β : Type ?u.752534
ι : Type ?u.752537
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f u : ℕ → α
n : ℕ
⊢ dist (∑ k in Finset.range (n + 1), u k) (∑ k in Finset.range n, u k) = ‖u n‖
simp [dist_eq_norm, sum_range_succ]