let m, x, y be Real; :: thesis: ( y > x & x >= 0 & m >= 0 implies x / y <= (x + m) / (y + m) )
assume that
A1: y > x and
A2: x >= 0 and
A3: m >= 0 ; :: thesis: x / y <= (x + m) / (y + m)
y - x > 0 by A1, XREAL_1:50;
then m * (y - x) >= 0 by A3;
then ((y * (x + m)) - (x * (m + y))) / (y * (y + m)) >= 0 by A1, A2, A3;
then ((x + m) / (y + m)) - (x / y) >= 0 by A1, A2, A3, XCMPLX_1:130;
then (((x + m) / (y + m)) - (x / y)) + (x / y) >= 0 + (x / y) by XREAL_1:6;
hence x / y <= (x + m) / (y + m) ; :: thesis: verum