mathlib

06f0d517 - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups (#8060)

refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups (#8060) This PR represents another wave of generalization of proofs, following from the `order` refactor. It is another step towards #7645.