Commit 2025-04-24 23:11 f962d8d3

View on Github →

chore: remove @[trans] annotations on orders (#24277) trans can use the Trans and IsTrans typeclasses to determine the transitivity of ≤ and <. So all these general @[trans] tags on these lemmas are redundant (or even bad). There is also a bug in trans that causes the tactic to not work with lemmas about ≤ and < that are tagged with @[trans], so these tags weren't doing anything anyways.

Estimated changes

modified theorem ge_trans
modified theorem gt_of_ge_of_gt
modified theorem gt_of_gt_of_ge
modified theorem gt_trans
modified theorem le_trans
modified theorem lt_of_le_of_lt
modified theorem lt_of_lt_of_le
modified theorem lt_trans