simp only [ge_iff_le, le_refl, Finset.Ioc_eq_empty_of_le]
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ Finset.Ioc k k = ∅
no goals