Commit 2022-01-19 10:24 4ad74aed
View on Github →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
.