theorem MeasureTheory.setLIntegral_Ioo_rpow {p : ℝ} {a b : ENNReal} (hp : -1 < p) : ∫⁻ (t : ENNReal) in Set.Ioo a b, t ^ p = (b ^ (p + 1) - a ^ (p + 1)) / ENNReal.ofReal (p + 1)

theorem MeasureTheory.setLIntegral_Iio_rpow {p : ℝ} {b : ENNReal} (hp : -1 < p) : ∫⁻ (t : ENNReal) in Set.Iio b, t ^ p = b ^ (p + 1) / ENNReal.ofReal (p + 1)