feat: BoundedAdd class for consistency with BoundedSub and BoundedMul.

[kkytola]

trafficstars

The classes BoundedSub and BoundedMul were added in PRs #12559 and #12790 to generalize subtraction and multiplication operations on bounded continuous functions (especially for the case of codomain NNReal). The existing generality for addition was sufficient, but in the review of #12790 it was pointed out that its assumption LipschitzAdd should probably be replaced for consistency by BoundedAdd (which is then a consequence of LipschitzAdd). This PR adds BoundedAdd and refactors the addition instances on bounded continuous functions accordingly, and additionally golfs the proofs of subtraction instances similarly using Lipschitzness.

---