mathlib3

f9f5d51e - feat(algebra/order/group): some more lemmas about `min`, `max`, and `abs` (#16485)

feat(algebra/order/group): some more lemmas about `min`, `max`, and `abs` (#16485) These are trivially true, but require a bit of annoying casework, making them handy to package into lemmas.