∀ {w : ℕ} (x y : BitVec w),
  (¬(if 2 * (x.toNat ^^^ y.toNat) < 2 ^ w then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)) =
        if x.toNat ^^^ y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)) →
    False