∀ (x y lo hi : ℤ),
  ¬x + y - lo -
          (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo + (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo) =
        (hi - lo) * ((x - lo) / (hi - lo)) + (hi - lo) * ((y - lo) / (hi - lo)) →
    False