theorem :: XREAL_1:21

for a, b, c, d being Real holds
( a + b <= c + d iff a - c <= d - b )