have l2 : ∑ x in Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x in Finset.range n, A (x + 1) * b (x + 1) :=
  Finset.sum_shift_front
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n