Commit 2025-06-07 17:32 f886ece7

View on Github →

chore(Order/Basic): move lemmas to the correct section (#25568) This PR moves some lemmas in Order.Basic to the correct place. Some of the lemmas now only assume LE or LT instead of Preorder. For example le_of_le_of_eq and le_of_le_of_eq' now have the same hypothesis.

Estimated changes

modified theorem le_of_eq_of_le'
modified theorem le_of_le_of_eq'
modified theorem lt_of_eq_of_lt'
modified theorem lt_of_lt_of_eq'