have := hC C (by simp)
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
this : ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ C * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)