Is there any idiom in mathcomp on how to declare a dual structure, containing all the definitions and lemmas as original one, without just copy-pasting it?

As a concrete example, I need to work with partial orders that have finite ideals:

https://github.com/Event-Structures/event-struct/blob/357797a38c368786717dacb8d88dc4bd247d0a70/theories/common/order.v#L427

Now I want to declare dual structure of partial orders with finite filters.

I want to obtain the same set of definitions and lemmas for the dual structure (modulo renaming `s/ideal/filter`

).

Last updated: Jan 29 2023 at 18:03 UTC