let a, b, c be real positive number ; :: thesis: ( a > b & b > c implies b / (a - b) > c / (a - c) )
assume that
A1: a > b and
A2: b > c ; :: thesis: b / (a - b) > c / (a - c)
A3: a - b > 0 by A1, XREAL_1:52;
b * (- 1) < c * (- 1) by A2, XREAL_1:71;
then (- b) + a < (- c) + a by XREAL_1:10;
then A4: c / (a - b) > c / (a - c) by A3, XREAL_1:78;
b / (a - b) > c / (a - b) by A2, A3, XREAL_1:76;
hence b / (a - b) > c / (a - c) by A4, XXREAL_0:2; :: thesis: verum