feat(analysis/special_functions/integrals): mul/div by a const (#6357)

This PR, together with #6216, makes the following possible:
```
import analysis.special_functions.integrals
open real interval_integral
open_locale real

example : ∫ x in 0..π, 2 * sin x = 4 := by norm_num
example : ∫ x:ℝ in 4..5, x * 2 = 9 := by norm_num
example : ∫ x in 0..π/2, cos x / 2 = 1 / 2 := by simp
```

src/analysis/special_functions/integrals.lean

@@ -20,6 +20,23 @@ This file is incomplete; we are working on expanding it.
 open real set interval_integral
 variables {a b : ℝ}
 
+namespace interval_integral
+variable {f : ℝ → ℝ}
+
+@[simp]
+lemma integral_const_mul (c : ℝ) : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x :=
+integral_smul c
+
+@[simp]
+lemma integral_mul_const (c : ℝ) : ∫ x in a..b, f x * c = (∫ x in a..b, f x) * c :=
+by simp only [mul_comm, integral_const_mul]
+
+@[simp]
+lemma integral_div (c : ℝ) : ∫ x in a..b, f x / c = (∫ x in a..b, f x) / c :=
+integral_mul_const c⁻¹
+
+end interval_integral
+
 @[simp]
 lemma integral_pow (n : ℕ) : ∫ x in a..b, x ^ n = (b^(n+1) - a^(n+1)) / (n + 1) :=
 begin