Commit 2025-09-08 12:49 30ce261d
View on Github →refactor: add a ≤ b + a field to CanonicallyOrderedAdd (#29084)
The only type of interest satisfying this typeclass without noncommmutative addition seems to be Ordinal. By requiring this extra field (which Ordinal does satisfy), we're able to generalize various theorems from the commutative to the noncommutative setting.