∀ {w : ℕ} {x y : BitVec w},
  (x.sdiv y).toFin =
    match x.msb, y.msb with
    | false, false => x.toFin / y.toFin
    | false, true => (-(x / -y)).toFin
    | true, false => (-(-x / y)).toFin
    | true, true => (-x).toFin / (-y).toFin