chore(algebra/order/sub): Generalize lemmas (#15497)
Generalize many lemmas from `canonically_ordered_add_monoid` to `has_exists_add_of_le`, and a few other generalizations.
### New lemmas
* `mul_le_cancellable_one`/`add_le_cancellable_zero`
* `tsub_add_le_right_comm`
* `add_tsub_add_le_tsub_left`
* `add_tsub_add_le_tsub_right`
