have := Ne.lt_of_le x_ne_b hx.2
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ x < ↑k + 1
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
this✝ : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
this : x < b
⊢ x < ↑k + 1