simpa using mul_le_mul l1 l2 zero_le_one (by simp)
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)
no goals