prove wordsToBytesToWords, and many prerequisite lemmas

Shows that inverting bytesToWords results in a list with the original
list as a prefix.

For the proof, defined dropWhile and proved various properties about it.
Also, proved some facts about l2n and LOG.