theorem :: XREAL_1:31

for a, b being Real st 0 <= a holds
b <= a + b