a + b > a + 0 by XREAL_1:6;
hence a div (a + b) is zero by NAT_D:27; :: thesis: verum