no goals
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n => dist (f n) (f (Nat.succ n))
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f (Nat.succ n))
simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0