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;