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.
`rew_tac` is expected to be filled in by something like `rewrite lem` (so to try two different things, you need to call it twice), while `repeat_rew_tac` should instead be trying both versions as much as possible, and therefore can be passed something like `progress rewrite ?lem, ?lem'`.