∀ {w : ℕ} (x y : BitVec w),
  x.smod y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      have u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      have u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)