Add a fold operation over finite maps, and associated lemmas

[fdupress]

No description provided.

[fdupress]

This is likely to stay WIP for a chunk. Useful bits could be pulled out as and when for merging.

[strub]

@fdupress Why not merging what is already there?

[fdupress]

Because it doesn't have the one thing I want: folding a function that is associative only over non-repeating lists.

We could merge this, but I don't think it brings much value yet.

[fdupress]

Sorry, that's an answer to "What are you waiting for?"

Why I don't merge what I have now is that I don't know if they are the right lemmas to have on this yet, and the project that would allow me to give it its trial by fire has been on hold for a bit.

[strub]

Let put this for the next meeting. bigop+perm_eq+uniq already provides this. Adding a thin layer on top of that could be sufficient.

[fdupress]

Conclusion to the meeting was: we need both your commit and what I want.

I was also due to undo the force push, but haven't gotten around to it yet. (Sorry!)