∀ (w : ℕ) {x y : BitVec (w + 1)},
  -2 ^ (w + 1) ≤ 2 * x.toInt →
    2 * x.toInt < 2 ^ (w + 1) →
      -2 ^ (w + 1) ≤ 2 * y.toInt →
        2 * y.toInt < 2 ^ (w + 1) →
          (-2 ^ (w + 1) ≤ x.toInt - y.toInt →
              x.toInt - y.toInt < 2 ^ (w + 1) →
                ((x.toInt - y.toInt).bmod (2 ^ (w + 1)) < 0 ↔
                  -(2 ^ (w + 1) / 2) ≤ x.toInt - y.toInt ∧ x.toInt - y.toInt < 0 ∨
                    (2 ^ (w + 1) + 1) / 2 ≤ x.toInt - y.toInt)) →
            0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ (w + 1)) < 0 → ¬2 ^ w ≤ x.toInt - y.toInt → False