chore(algebra/order/sub): Generalize to `preorder` and `add_comm_semigroup` (#11463)
This generalizes a bunch of lemmas from `partial_order` to `preorder` and from `add_comm_monoid` to `add_comm_semigroup`.
It also adds `tsub_tsub_le_tsub_add : a - (b - c) ≤ a - b + c`.