simp_rw [div_eq_inv_mul]
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N.log / Real.log 2) =O[atTop] fun N => N.log
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