feat(algebra/bounds): a few lemmas like bdd_above (-s) ↔ bdd_below s (#8522)
bdd_above (-s) ↔ bdd_below s