let y, x, m be real number ; :: thesis: ( y > x & x >= 0 & m >= 0 implies x / y <= (x + m) / (y + m) )
assume A1: ( y > x & x >= 0 & m >= 0 ) ; :: thesis: x / y <= (x + m) / (y + m)
then y - x > 0 by XREAL_1:52;
then A2: m * (y - x) >= 0 by A1;
y * (y + m) > 0 by A1;
then ((y * (x + m)) - (x * (m + y))) / (y * (y + m)) >= 0 by A2;
then ((x + m) / (y + m)) - (x / y) >= 0 by A1, XCMPLX_1:131;
then (((x + m) / (y + m)) - (x / y)) + (x / y) >= 0 + (x / y) by XREAL_1:8;
hence x / y <= (x + m) / (y + m) ; :: thesis: verum