Finite map composition
- Add a
map_compose
operator for finite map composition - Add notation
m ∘ₘ n
formap_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
).