Commit 2025-12-24 14:13 155c3639
View on Github →chore: more to_dual tags on Order.(succ/pred) (#33150)
I had to change some proofs to use succ_le_succ instead of succ_mono, since the latter can't yet be dualized. In the future, we should probably deprecate the former.