feat(order/bounded_order): with_top.of_dual (#15727)
`with_top.to_dual : with_top α ≃ with_bot αᵒᵈ`
Also define
* `with_top.of_dual`
* `with_bot.to_dual`
* `with_bot.of_dual`
API on the application of these added,
their relation to `le` and `lt`,
and how they interact with `with_{bot,top}.map`
Some `with_top` proofs that broke through the `option` or `order_dual` API
have been rephrased to carry over the `with_bot` proofs across these functions.
