Commit 2025-12-18 23:55 29f37a66

chore(Order/WithBot): add to_dual attributes (part 2) (#32626) Some design considerations:

• The ≤ and < instances on WithBot and WithTop are were deliberately made def-eq. I've not changed this, which results in some awkward code before we develop the API to hide this.
• There was some major disparity in the unbot and untop API. I had to add a bunch of lemmas to amend it.
• I reordered a few theorems to avoid having to constantly open and close the WithBot namespace.