norm_cast
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑↑b ^ (-s + 1) - ↑↑a ^ (-s + 1)) / (-s + 1)
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑b ^ (-s + 1) - ↑a ^ (-s + 1)) / (-s + 1)