simp only [Asymptotics.isBigO_top, Real.norm_eq_abs]
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
⊢ f =O[⊤] g
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|