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