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.

It might be better, at some point, to switch to [more systematic existing tactics from prior work](http://arxiv.org/pdf/1106.4448.pdf) which is [on opam](https://github.com/coq/repo-stable/tree/master/packages/coq:aac-tactics/coq:aac-tactics.1.0.0), but I was sufficiently close to having working Ltac code that I figured I'd just make what I had work.

We might or might not want to move the unicode versions of the tactics elsewhere.

This closes #536.
Comment included.