ring
case h.e'_3.h
x✝¹ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℂ
⊢ ↑x ^ x✝ / (x✝ + 1) - (↑x)⁻¹ / (x✝ + 1) = (↑x ^ x✝ - (↑x)⁻¹) / (x✝ - -1)
no goals