refine ZetaSum_aux1_2 (c := s.re) apos a_lt_b ⟨ne_of_gt σpos, ?_⟩
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1) = (a ^ (-s.re) - b ^ (-s.re)) / s.re
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ 0 ∉ [[a, b]]