exact div_nonneg (by norm_num) (norm_nonneg s)
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ 0 ≤ 1 / ‖s‖
no goals