Reverse/Dual/Opposite of an order

[hivert]

Note on what we discussed at Dagstuhl 18341:

• The name "reverse" order looks bad to me. Indeed the reverse lexicographic order is not the reverse of the lex order. My vote goes for "dual". "opposite" is also ok.
• dual of finite (porder/order/lattice) should be canonically finite.

Cheers,

Florent