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.





leanprover-community/mathlib,leanprover-community/mathlib