Commit 2022-06-06 18:41 7b7da893
View on Github →feat(algebra/order/*): typeclass for 0 ≤ 1 (#14510)
With this new typeclass, lemmas such as zero_le_two and one_le_two can be generalized to require just a few typeclasses for notation, zero_add_class, and some covariant class.