Add solver `multiset_solver` for multisets

The code contains some documentation how it works.

I added a number of tests, and used it to automate many existing lemmas in the gmultiset file.

Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section basic_lemmas) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section multiset_unfold). None of the lemma statements changed, only many proofs are replaced by a mere call to multiset_solver.

/cc @msammler