congr
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))
case e_a
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s = (starRingEnd ℂ) (↑x ^ s)