mathlib3

feat(algebra/order): allow simp to flip inequalities

#1418

Merged