theorem :: XREAL_1:32

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