hooking word into lia

[JasonGross]

Should https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ZnWords.v be adapted to hook into the zify mechanism a la https://github.com/coq/coq/blob/master/theories/micromega/ZifyUint63.v and be integrated into coqutil?

[samuelgruetter]

Migrating ZnWords to coqutil would be ok with me.

Since ZnWords is supposed to work for every word n if n is a concrete constant, we would need parameterized zify typeclass instances, and the last time I tried to do that (not for ZnWords, but for LittleEndian), Frédéric Besson said

Don't expect zify to work with parameterized instances. Some error checking is missing but the error message should be something like "Dependent types are not allowed".
This is a strong restriction of the implementation that is hardwired very deep. Sorry.

Maaaybe we could duplicate the Add Zify ... commands for each word size of interest, but what if the word instance is a section variable? Use Load? Not sure if that's worth the trouble at the moment.