theorem :: ASYMPT_2:17

for a, b being Nat st a <= b holds
seq_n^ a in Big_Oh (seq_n^ b)