rw [Asymptotics.isBigO_atTop_iff_eventually_exists] at h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : ∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|