Finite map composition

• Add a map_compose operator for finite map composition
• Add notation m ∘ₘ n for map_compose m n
• Add various lemmas to manipulate map composition

This is arguably a niche operator we might not want to include. If you think that is the case feel free to close without merging.

I'm submitting in case someone else would have a use for it, since this is now fairly complete (although it could use some compatibility lemmas with insert).