ex s, s1 being eventually-positive Real_Sequence st
( s = seq_a^ (2,1,0) & s1 = seq_a^ (2,1,1) & Big_Oh s = Big_Oh s1 )