simp_rw [cumsum, add_comm _ N, Finset.sum_range_add]
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ cumsum (fun i => u (i + N)) n = cumsum u (n + N) - cumsum u N
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ ∑ x ∈ Finset.range n, u (N + x) =
    ∑ x ∈ Finset.range N, u x + ∑ x ∈ Finset.range n, u (N + x) - ∑ x ∈ Finset.range N, u x