Specific integrals

Stream: Is there code for X?

[Jason KY.]

Do we have lemmas about specific integrals such as

lemma interval_integral_pow (p : ℕ) (x : ℝ) :
  ∫ t in 0..x, t ^ p = (p + 1 : ℝ)⁻¹ * x ^ (p + 1) :=

I need this for the tail probability formula. If not, where should I put them (interval_integral maybe or a new file)?