linarith
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
⊢ b - ε / 2 < b
no goals