for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) = 0 holds
( f in Big_Oh g & not g in Big_Oh f )