specialize hN N le_rfl
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∃ c, ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|