Added a few miscellaneous group theory and word lemmas:

[sjjs7]

    ABELIAN_GROUP_PRODUCT_ITERATE
    ABELIAN_GROUP_SUM_ITERATE
    GROUP_HOMOMORPHISM_PRODUCT
    GROUP_HOMOMORPHISM_PRODUCT_INJECTION
    GROUP_HOMOMORPHISM_SUM
    GROUP_HOMOMORPHISM_SUM_INJECTION
    GROUP_HOMOMORPHISM_SUM_PROJECTION
    INT_VAL_WORD_MASK
    REAL_VAL_WORD_MASK
    REAL_VAL_WORD_NEG_CASES
    SUM_GROUP_ALT
    VAL_WORD_MASK

Also made a couple of changes in the existing group theory material to emphasize the newer "group_sum G" in place of "iterate (group_add G)", renaming ABELIAN_GROUP_SUM to ABELIAN_GROUP_ITERATE while also removing its finiteness assumption:

ABELIAN_GROUP_ITERATE = |- !G x k. abelian_group G /\ (!i. i IN k ==> x i IN group_carrier G) ==> iterate (group_add G) k x IN group_carrier G

and changing ABELIAN_GROUP_HOMOMORPHISM_GROUP_SUM to use "group_sum" explicitly:

ABELIAN_GROUP_HOMOMORPHISM_GROUP_SUM = |- !f k A B. abelian_group B /\ (!i. i IN k ==> group_homomorphism (A i,B) (f i)) ==> group_homomorphism (sum_group k A,B) (\x. group_sum B k (\i. f i (x i)))

Also dded a simple tactic (naive backchaining plus optional initial polynomial normalization) to "Library/floor.ml" that tries to prove a real expression is an integer

    # g `integer(&22 / &7 * (x - x * &1) + &n pow 7)`;;
    ...
    # e REAL_INTEGER_TAC;;
    val it : goalstack = No subgoals

[JacquesCarette]

Should I wait for your 'ok' before merging this, is do you think it's ready to go?

[sjjs7]

I will check it first.

[sjjs7]

Alright looks ok to merge.