[Merged by Bors] - feat(algebra/order/sub): An add_group has ordered subtraction

[YaelDillies]

This wraps up sub_le_iff_le_add in an has_ordered_sub instance.

---

[eric-wieser]

Does it make more sense to do this in the other direction, and have group import sub?

[YaelDillies]

I think so too! because then we can also deduplicate the two lemmas: we get rid of sub_le_iff_le_add and rename tsub_le_iff_right to sub_le_iff_right or sub_le_iff_le_add.
What do you think?

[eric-wieser]

I'd leave the renaming for another PR, but I think it probably makes sense.

[fpvandoorn]

I think this instance is indeed good to add.

I'm not sure if I'm in favor of renaming tsub_le_iff_right. It depends a bit on how much lemmas will be general enough to apply in both cases. Many lemmas that hold for group require canonically_ordered_add_monoid in the order.sub file, so we will have to keep them as duplicates. And many other lemmas need extra assumptions in the has_ordered_sub case. So if there are only a couple of lemmas that are the same for has_ordered_sub / add_group, then I would keep both names (with sub and with tsub). We can of course still make the sub lemmas aliases of the tsub lemmas.
If there are a lot (which I don't expect), we could reconsider.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests