mathlib3

feat(algebra/order_functions): max_lt_max and min_lt_min

#692

Merged