mathlib

d558350f - feat(algebra/ordered_group): add a few instances, prune unneeded code (#8075)

feat(algebra/ordered_group): add a few instances, prune unneeded code (#8075) This PR aims at shortening the subsequent `order` refactor. The removed lemmas can now by proven as follows: ```lean @[to_additive ordered_add_comm_group.add_lt_add_left] lemma ordered_comm_group.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b := mul_lt_mul_left' h c @[to_additive ordered_add_comm_group.le_of_add_le_add_left] lemma ordered_comm_group.le_of_mul_le_mul_left (h : a * b ≤ a * c) : b ≤ c := le_of_mul_le_mul_left' h @[to_additive] lemma ordered_comm_group.lt_of_mul_lt_mul_left (h : a * b < a * c) : b < c := lt_of_mul_lt_mul_left' h ``` They were only used in this file and I replaced their appearances by the available proofs.