begin
Lm1:
for f, g being Real_Sequence
for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n)
begin
Lm2:
for f, g being eventually-nonnegative Real_Sequence holds
( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g )
Lm3:
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
f in Big_Oh g
begin
begin
begin