linarith [h_mem hs]
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
s : ℂ
x✝² : s ∈ Square (-1) c \ {-1}
hs : s ∈ Square (-1) c
hs1 : s ∉ {-1}
x✝¹ : s.re = 0
x✝ : s.im = 0
⊢ False
no goals