let a, b, c, d be positive Real; :: thesis: ( b > a & c > d implies c / (c + a) > d / (d + b) )
assume that
A1: b > a and
A2: c > d ; :: thesis: c / (c + a) > d / (d + b)
b * c > a * d by A1, A2, XREAL_1:96;
then (b * c) + (c * d) > (a * d) + (c * d) by XREAL_1:8;
then c * (b + d) > d * (a + c) ;
hence c / (c + a) > d / (d + b) by XREAL_1:106; :: thesis: verum