Commit 2024-10-08 07:22 688ff147

feat: ring-based prover for certain inequalities in semirings (#16840) This PR provides automation for proving certain kinds of inequalities in commutative semirings: goals of the form A ≤ B and A < B for which the ring-normal forms of A and B differ by a nonnegative (resp. positive) constant. For example, ⊢ x + 3 + y < y + x + 4 is in scope because the normal forms of the LHS and RHS are, respectively, 3 + (x + y) and 4 + (x + y), which differ by a constant. This automation is not intended to be user-facing. Rather, it will serve as the discharger tactic for the linear_combination tactic on inequality goals.