Commit 2026-02-13 04:47 c5134ef9

chore: use @[to_dual] in Bounds.Basic (#35208) This PR adds @[to_dual] name dictionary entries for atom/coatom and lfp/gfp, and uses @[to_dual] to auto-generate dual theorems in Order.Bounds.Basic, deleting the hand-written versions. 27 @[to_dual] annotations total, deleting 27 hand-written duals. Remaining pairs not converted:

• bddAbove_insert/bddBelow_insert — needs directed/codirected dictionary entry, which causes problems elsewhere
• IsLUB.exists_between/IsGLB.exists_between — @[to_dual] swaps the And conjuncts
• Bounded interval theorems (Icc, Ico, etc.) — arguments swap under duality
• DenselyOrdered interval theorems — dual proofs need simpa [Ioo_toDual]
• isGreatest_himp/isLeast_sdiff — needs himp/sdiff dictionary entry 🤖 Prepared with Claude Code