let r := -s - 1
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x