convert integrability_aux₁.add integrability_aux₂ using 2
a b : ℝ
⊢ IntervalIntegrable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) MeasureTheory.volume a b
case h.e'_3.h
a b x✝ : ℝ
⊢ ↑⌊x✝⌋ + 1 / 2 - ↑x✝ = ↑⌊x✝⌋ + (1 / 2 - ↑x✝)