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