for a, b being Real st a >= b holds
(a -' b) + b = a