apply ((isBigO_refl ..).const_mul_left ..).add
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)) =O[atTop] fun N => ↑N / (↑N).log
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 6 * (↑x ^ (1 / 2) * (1 + 1 / 2 * (↑x).log) ^ 3)) =O[atTop] fun N => ↑N / (↑N).log