for a, b being Nat st a <= b holds
seq_n^ a in Big_Oh (seq_n^ b)