Update src/Init/Data/BitVec/Bitblast.lean

Co-authored-by: Alex Keizer <alex@keizer.dev>

src/Init/Data/BitVec/Bitblast.lean

@@ -513,7 +513,7 @@ structure DivModState (w : Nat) : Type where
   r : BitVec w
 
 /-- A `DivModState` is lawful if the remainder width `wr` plus the dividend width `wn` equals `w`,
-and that the bitvectors `r` and `n` have values in these bounds given these bitwidths.
+and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`.
 
 This is a proof engineering choice: An alternative world could have
 `r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions.