mathlib3

8ef2c02c - chore(order/bounded_order): move `order_dual` instances up, use them to golf lemmas (#14544)

chore(order/bounded_order): move `order_dual` instances up, use them to golf lemmas (#14544) I only golf lemmas and `Prop`-valued instances to be sure that I don't add `order_dual`s to the statements.