:: deftheorem defines is_smooth_wrt ASYMPT_0:def 16 :
for f being eventually-nonnegative Real_Sequence
for b being Nat holds
( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );