ring_nf
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..↑k + 1, φ x) + (↑k + 1 + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..↑k + 1, φ x)
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (1 + k), φ ↑x = φ (1 + ↑k)