for x, y, z being ExtReal st x is real holds
( y + x <= z iff y <= z - x )