a + b > a + 0 by XREAL_1:6;
hence a mod (a + b) = a by NAT_D:63; :: thesis: verum