Commit 2025-01-04 21:33 80fa5c2e
View on Github →chore(SetTheory/Ordinal/Arithmetic): IsLeftCancelAdd Ordinal (#19888)
In general, AddLeftMono + AddLeftReflectLE + PartialOrder → IsLeftCancelAdd, but this feels like too niche of a situation to create the general instance.