mathlib3

34a9d0df - feat(algebra/order/ring): Binary rearrangement inequality (#14478)

feat(algebra/order/ring): Binary rearrangement inequality (#14478) Extract the binary case of the rearrangement inequality (`a * d + b * c ≤ a * c + b * d` if `a ≤ b` and `c ≤ d`) from the general one.