for c being non negative Real
for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds
x in Big_Oh (c + f)