> wordsLib.BITS_INTRO_CONV ``(n DIV 16) MOD 4``;
val it = |- (n DIV 16) MOD 4 = BITS 5 4 n: thm

> wordsLib.BITS_INTRO_CONV ``n MOD 16 DIV 4``;
val it = |- n MOD 16 DIV 4 = BITS 3 2 n: thm

> wordsLib.BITS_INTRO_CONV ``n MOD 16``;
val it = |- n MOD 16 = BITS 3 0 n: thm

> wordsLib.BITS_INTRO_CONV ``n MOD dimword(:'a)``;
val it =
   |- n MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 n:
   thm