mathlib3

5de67573 - chore(algebra/ordered_group): deduplicate (#5403)

chore(algebra/ordered_group): deduplicate (#5403) I deleted many `a_of_b` lemmas for which `a_iff_b` existed, then restored (most? all?) of them using `alias` command.