intervalIntegral_inv_sq_of_pos

theorem intervalIntegral_inv_sq_of_pos {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :    ∫ x in a..b, (x ^ 2)⁻¹ = a⁻¹ - b⁻¹ := by  have hpos_uIcc : ∀ x ∈ Set.uIcc a b, 0 < x := by    intro x hx    rw [Set.uIcc_of_le hab] at hx    exact ha.trans_le hx.1  have hderiv : ∀ x ∈ Set.uIcc a b,      HasDerivAt (fun y : ℝ => -y⁻¹) ((x ^ 2)⁻¹) x := by    intro x hx    have h : HasDerivAt (fun y : ℝ => -y⁻¹) (-(-(x ^ 2)⁻¹)) x :=      (hasDerivAt_inv (hpos_uIcc x hx).ne').neg    rwa [neg_neg] at h  have hint : IntervalIntegrable (fun x : ℝ => (x ^ 2)⁻¹) volume a b := by    apply ContinuousOn.intervalIntegrable_of_Icc hab    exact (continuousOn_pow 2).inv₀ fun x hx => by      exact pow_ne_zero 2 (hpos_uIcc x (by simpa [Set.uIcc_of_le hab] using hx)).ne'  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hderiv hint]  ring