Add tactics for rewriting modulo associativity

They're somewhat ad-hoc, and probably need more documentation and
examples and test cases, but the basic examples work, and I've left this
laying around for far too long.

This closes #536.
Add some comments to RewriteModuloAssociativity.v

From Mike Shulman's suggestions
Use left association rather than right association

The notations for composition and concatenation are built for left
association.
Merge pull request #607 from JasonGross/rewrite-modulo-associativity

Add tactics for rewriting modulo associativity