∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ ∑' (m : ℕ), d m