feat(analysis/convex/*): Convexity and subtraction (#14015)
Now that we have a fair bit more pointwise operations on `set`, a few results can be (re)written using them. For example, existing lemmas about `add` and `neg` can be combined to give lemmas about `sub`.
