Commit 2026-03-23 08:24 e342913b

chore(Order/UpperLower/Closure): use to_dual (#36969) This PR tags upperClosure with to_dual.

• to_dual was not happy with the proof of upperClosure_image. I replaced it with a proof with less defeq abuse, by tagging UpperSet.map with simps.
• to_dual is not happy with the galois connections, because they are between the order and a set-containment order, and only one of the two is translated by to_dual. Hence, the proofs using the galois connection cannot be translated automatically, and we need to use to_dual existing. I changed two proofs to avoid this dependency.
• I changed the to_dual_insert_cast proof of GaloisInsertion to clarify what is going on there.
• DecidablePred was being translated to DecidableSucc, so I added a fix in the abbreviation dictionary.