feat(order/basic): Antitone functions (#9119)
Define `antitone` and `strict_anti`. Use them where they already were used in expanded form. Rename lemmas accordingly.
Provide a few more `order_dual` results, and rename `monotone.order_dual` to `monotone.dual`.
Restructure `order.basic`. Now, monotone stuff can easily be singled out to go in a new file `order.monotone` if wanted. It represents 587 out of the 965 lines.
