∀ {w i : ℕ} {x y : BitVec w} (h : i < w),
  (x.smod y)[i] =
    match x.msb, y.msb with
    | false, false => (x % y)[i]
    | false, true => (if x % -y = 0#w then x % -y else x % -y + y)[i]
    | true, false => (if -x % y = 0#w then -x % y else y - -x % y)[i]
    | true, true => (-(-x % -y))[i]