summation_by_parts

lemma summation_by_parts {E : Type*} [Ring E] {a A b : ℕ → E} (ha : a = nabla A) {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 := by  have 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 :=    Finset.sum_shift_back  have l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n,      A (x + 1) * b (x + 1) :=    Finset.sum_shift_front  simp only [cumsum, ha, Pi.mul_apply, nabla, sub_mul, Finset.sum_sub_distrib, l1, l2, shift,    mul_sub]  abel