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