∀ {w : ℕ} (qr : BitVec.DivModState w) (n d : BitVec w),
  BitVec.divSubtractShift { n := n, d := d } qr =
    if qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d then
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false, r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }
    else
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat true,
        r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) - d }