theorem :: ASYMPT_2:32

for k, n being Nat st k <= n holds
Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n)