The key is the framing; as stated, x and y are _exact_ floating-point values, which makes the statement true[1]. In fact, it's embarrassingly trivial, since it

The key is the framing; as stated, x and y are _exact_ floating-point values, which makes the statement true[1]. In fact, it's embarrassingly trivial, since it is just a weakening of the definition of rounding used by IEEE 754. In particular, if cancellation occurs in x - y, then the result is exact (Sterbenz' lemma). [1] Under the assumption that no underflow or overflow occurs (which is the usual framing for this sort of naive error analysis). It's easy enough to correct for underflow by adding an absolute error term as well.