subword of word y at position pos into x (with a result possibly another
wordsize), together with one basic lemma, and support in BIT_WORD_CONV
and WORD_RED_CONV/WORD_REDUCE_CONV. Also added a fairly large number
of additional lemmas about "word_popcount" (population count, Hamming
weight) including its subadditivity (WORD_POPCOUNT_ADD). New definition:

        word_insert

and theorems

        BITS_OF_WORD_SUBSET
        BITS_OF_WORD_SUBSET_ALT
        BITS_OF_WORD_SUBSET_NUMSEG
        BIT_WORD_INSERT
        BIT_WORD_JOIN_GEN
        NUMSEG_LT_DIMINDEX
        VAL_LE_SUBSET
        WORD_OF_BITS_EMPTY
        WORD_POPCOUNT_ADD
        WORD_POPCOUNT_ADD_DISJOINT
        WORD_POPCOUNT_ADD_OR
        WORD_POPCOUNT_AND
        WORD_POPCOUNT_BITVAL
        WORD_POPCOUNT_BOUND_SIZE
        WORD_POPCOUNT_LE_BITS
        WORD_POPCOUNT_NSUM
        WORD_POPCOUNT_OR
        WORD_POPCOUNT_OR_AND
        WORD_POPCOUNT_OR_DISJOINT
        WORD_POPCOUNT_SHL
        WORD_POPCOUNT_USHR
        WORD_POPCOUNT_WORD_OF_BITS
        WORD_POPCOUNT_WORD_OF_BITS_GEN
        WORD_POPCOUNT_XOR
        WORD_POPCOUNT_XOR_AND
        WORD_POPCOUNT_XOR_AND2