feat(to_additive): support (attr := reassoc)

[JovanGerb]

This PR uses registerGeneratingAttr, so that to_additive (attr := reassoc) also tags the _assoc lemma with to_additive.

This interacts awkwarly with to_dual (attr := reassoc), because in that case, the reassoc attribute is responsible for handling the to_dual attribute. This is solved by adding a check so that we only insert a new translation if it doesn't already exist (e.g. because reassoc could have added it).

---

[github-actions]

PR summary 3144a34bda

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ reassocImpl

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[chrisflav]

Thanks! Looks good to me, but I am in no way competent to review this.

[chrisflav]

There is the same issue in Monoidal/Mon.lean. Could you please also fix that one?