Commit 2025-12-02 14:25 7b4930f0

View on Github →

chore(Order/RelClasses): use @[to_dual] (#32090) This PR tags WellFoundedLT and WellFoundedGT with @[to_dual]. It also improves the name guessing so that these names are translated into eachother. The automatically generated form doesn't use GE.ge or GT.gt, but instead swaps the arguments of LE.le and LT.lt. Arguably, this is an improvement.

Estimated changes

deleted theorem WellFoundedGT.apply
deleted def WellFoundedGT.fix
deleted theorem WellFoundedGT.fix_eq
deleted theorem WellFoundedGT.induction
deleted theorem transitive_ge
deleted theorem transitive_gt
deleted theorem wellFoundedLT_dual_iff
deleted theorem wellFounded_gt