Commit 2025-12-05 03:30 b6ceecfe

chore(Order/Lattice): use to_dual for SemilatticeSup (#32321) This PR uses to_dual for SemilatticeSup Notes:

• to_dual cannot handle Monotone for the same reason that it cannot handle DecidableLT.
• The dual of le_iff_exists_sup did not exist before.
• The dual of le_of_sup_eq did not exist before.
• sup_le_sup_left, sup_congr_left, sup_eq_sup_iff_left et all use the wrong left/right naming convention.
• sup_le_sup_left, sup_le_sup_right currently require (reorder := h₁ c), which indicates that the argument order is fishy.