let a, b be Nat; :: thesis: ( a <= b implies seq_n^ a in Big_Oh (seq_n^ b) )
assume AS: a <= b ; :: thesis: seq_n^ a in Big_Oh (seq_n^ b)

per cases ( a = b or a < b ) by AS, XXREAL_0:1;

suppose a = b ; :: thesis: seq_n^ a in Big_Oh (seq_n^ b)

hence seq_n^ a in Big_Oh (seq_n^ b) by ASYMPT_0:10; :: thesis: verum

end;

suppose a < b ; :: thesis: seq_n^ a in Big_Oh (seq_n^ b)

hence seq_n^ a in Big_Oh (seq_n^ b) by FROMASYMPT1t11; :: thesis: verum

end;

end;