mathlib3

7b7da893 - feat(algebra/order/*): typeclass for `0 ≤ 1` (#14510)

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.