refine EventuallyEq.trans_isBigO ?_ nabla_log_main
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =O[atTop] fun x => 1 / x
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =ᶠ[atTop] nabla Real.log