for a, b being positive Real st a < b holds
not seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0))