seq_n^ 2 in Big_Oh (seq_n^ 3)