apply IsBigO.mul
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * (1 + N.log / Real.log 2)) =O[atTop] fun N => N ^ (1 / 2) * N.log
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2)) =O[atTop] fun x => x ^ (1 / 2)

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 1 + x.log / Real.log 2) =O[atTop] fun x => x.log