mathlib3
3b3cd894 - chore(order/cover): add `covby.eq_of_between` (#17146)

Commit

3 years ago

chore(order/cover): add `covby.eq_of_between` (#17146) Also add some trivial lemmas about covby on int, for convenience.

Author

eric-wieser

Parents