∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {a b : ℝ},
  0 ≤ a →
    a ≤ b →
      (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) →
        MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume →
          ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
            f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Finset.Icc 0 ⌊a⌋₊, c k -
              ∫ (t : ℝ) in Set.Ioc a b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k