ex s being eventually-positive Real_Sequence st
( s = seq_a^ (2,2,0) & Big_Oh s c= Big_Oh (seq_n! 0) & not Big_Oh s = Big_Oh (seq_n! 0) )