theorem mul_isBigO_mul {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedDivisionRing E] {f g F G : α → E} (hf : f =O[Filter.atTop] F) (hg : g =O[Filter.atTop] G) : (f * g) =O[Filter.atTop] (F * G)

theorem isBigO_pow {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedDivisionRing E] {f F : α → E} {n : ℕ} (hf : f =O[Filter.atTop] F) : (fun (x : α) => f x ^ n) =O[Filter.atTop] fun (x : α) => F x ^ n