theorem :: XREAL_1:45

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