summable_iff_bounded'

lemma summable_iff_bounded' {u : ℕ → ℝ} (hu : ∀ᶠ n in atTop, 0 ≤ u n) :    Summable u ↔ BoundedAtFilter atTop (cumsum u) := by  obtain ⟨N, hu⟩ := eventually_atTop.mp hu  have e2 : cumsum (fun i ↦ u (i + N)) = fun n => cumsum u (n + N) - cumsum u N := by    ext n ; simp_rw [cumsum, add_comm _ N, Finset.sum_range_add] ; ring  rw [← summable_nat_add_iff N, summable_iff_bounded (fun n => hu _ <| Nat.le_add_left N n), e2]  simp_rw [sub_eq_add_neg, BoundedAtFilter.add_const, BoundedAtFilter.comp_add]