specialize h (c := 2⁻¹) (by norm_num)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ f =O[atTop] (f + g)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ f =O[atTop] (f + g)