{w : ℕ} →
  {args : BitVec.DivModArgs w} →
    {qr : BitVec.DivModState w} →
      {motive : BitVec.DivModState.Poised args qr → Sort u} →
        (t : BitVec.DivModState.Poised args qr) →
          ((toLawful : BitVec.DivModState.Lawful args qr) → (hwn_lt : 0 < qr.wn) → motive ⋯) → motive t