Possible consolidation with mathcomp-finmap

[palmskog]

As discussed in this Coq Platform issue, exstructures has overlaps with mathcomp-finmap in terms of notations, structures, and results. Hence, it would be beneficial to the Coq community if some kind consolidation or partitioning happened between the two projects, e.g., exstructures started depending on finmap and complementing it. However, such an integration process should take into account the interests of all stakeholders.

We recently started an effort to track and coordinate consolidation efforts like this in the Coq community. I open this issue to enable this tracking in a better way and since it could be a better place for discussion than the Coq Platform issue.