reconsider c = a + b as positive Real ;
reconsider d = a + (2 * b) as positive Real ;
a + b > a + 0 by XREAL_1:6;
then a / (a + b) <= (a + b) / ((a + b) + b) by SERIES_3:1;
then (d / c) * (a / c) <= (d / c) * (c / d) by XREAL_1:64;
then (d / c) * (a / c) <= 1 by XCMPLX_1:112;
then (d * a) / (c * c) <= 1 by XCMPLX_1:76;
hence not ((a + (2 * b)) * a) / ((a + b) |^ 2) is heavy by NEWTON:81; :: thesis: verum