simp  at l
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = Integrable.integral f a a + Integrable.integral f a a
⊢ Integrable.integral f a a = 0
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = 0
⊢ Integrable.integral f a a = 0