convert hasDerivAt_neg' s |>.const_cpow (c := N) (by aesop) |>.neg |>.div_const _ using 1
N : ℕ
Npos : 0 < N
s : ℂ
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (-(-↑(↑N).log * ↑N ^ (-s)) / 2) s
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
⊢ -(-↑(↑N).log * ↑N ^ (-s)) / 2 = -(↑N ^ (-s) * (↑N).log * -1) / 2