Commit 2021-06-29 17:54 d558350f

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:

@[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.