simp [div_rpow_eq_rpow_neg _ _ _ this, sub_eq_add_neg, add_comm]
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this✝ : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
x : ℝ
hx : x ∈ [[a, b]]
this : 0 ≤ x
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
no goals