fix(Algebra/GroupWithZero/Associated): de-abbrev Associates

[SnirBroshi]

Associates is an abbrev for Quotient _, but there are many instances defined on it.
Some of them create diamonds with general Quotient instances: Inhabited, Unique, and most notably Preorder.

While Associates has a Preorder instance that uses the divisibility relation, any monoid with a Preorder will have its ordering lifted to the Quotient. So currently Associates ℕ has two different LE orders defined on it that disagree on 2 ≤ 3.

This changes Associates to a def tagged with @[implicit_reducible].

---

The nonZeroDivisors proof is now a bit awkward, since the Equiv works for Quotients but simp refuses to evaluate the Equiv because Associate elements are multiplied but Quotient doesn't have that multiplication. Though rw works thanks to @[implicit_reducible].

[github-actions]

PR summary e23e51da8d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ quotient_out

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
6986	-1	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit e23e51da8d
Reference commit 375d54da29

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).