I don't think that's a good example, since it's obviously provably true and the proof is also obvious (either use well-known lemmas like log(poly(x)) in O(x^a)

I don't think that's a good example, since it's obviously provably true and the proof is also obvious (either use well-known lemmas like log(poly(x)) in O(x^a) or show that lim_x->inf lhs/x = 0 via L'Hôpital's rule, differentiation algorithms and well-known limits at infinity).