theorem :: ASYMPT_1:31

( Big_Oh (seq_n! 0) c= Big_Oh (seq_n! 1) & Big_Oh (seq_n! 0) <> Big_Oh (seq_n! 1) )