chore(order/bounded_order): Golf `disjoint` API (#14194)
Reorder lemmas and golf.
Lemma additions:
* `disjoint.eq_bot_of_ge`
* `is_compl.of_dual`
* `is_compl_to_dual_iff`
* `is_compl_of_dual_iff`
Lemma deletions:
* `eq_bot_of_disjoint_absorbs`: This is an unhelpful combination of `disjoint.eq_bot_of_ge` and `sup_eq_left`
* `inf_eq_bot_iff_le_compl`: This is a worse version of `is_compl.disjoint_left_iff`
Lemma renames:
* `is_compl.to_order_dual` → `is_compl.dual`
