∀ {m : ℕ} (x y : BitVec m),
  x.smod y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      have u := x.umod y.neg;
      if u = BitVec.zero m then u else u.add y
    | true, false =>
      have u := x.neg.umod y;
      if u = BitVec.zero m then u else y.sub u
    | true, true => (x.neg.umod y.neg).neg