apply IsBigO.const_mul_left
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => (Real.log 2)⁻¹ * N.log) =O[atTop] fun N => N.log
case h₂.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x.log) =O[atTop] fun N => N.log