for n being Nat holds n --> 0 is dominated_by_0 by Lm2;