for m, x, y being Real st y > x & x >= 0 & m >= 0 holds
x / y <= (x + m) / (y + m)