a + b >= a + 0 by XREAL_1:6;
hence not a / (a + b) is heavy by XREAL_1:185; :: thesis: verum