let a, b, c be Real; :: thesis: ( a <= b & b > 0 & c >= 0 implies a / b <= (a + c) / (b + c) )
assume A1: ( a <= b & b > 0 & c >= 0 ) ; :: thesis: a / b <= (a + c) / (b + c)
then a * c <= b * c by XREAL_1:64;
then (a * b) + (a * c) <= (a * b) + (b * c) by XREAL_1:6;
then a * (b + c) <= b * (a + c) ;
hence a / b <= (a + c) / (b + c) by XREAL_1:102, A1; :: thesis: verum