constructor
case a
φ : ℝ → ℂ
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
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1
case a.mp
φ : ℝ → ℂ
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
m : ℤ
⊢ k < m ∧ m ≤ 1 + k → m = k + 1

case a.mpr
φ : ℝ → ℂ
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
m : ℤ
⊢ m = k + 1 → k < m ∧ m ≤ 1 + k