Commit 2026-05-04 14:03 b26e5805

feat(positivity): positivity extension for a - b (#36401) This PR adds support in positivity for proving things about subtraction. For example, if the goal is 0 < a - b, and there is a local hypothesis of type b < a, then we close the goal. The motivation is that we want positivity to be a flexible tactic. So, when trying to prove 0 < a - b using a local hypothesis, we should look for the simp normal form of this, which is b < a.