Commit 2022-06-09 19:45 34a9d0df

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.