feat(algebra/to_additive): map pow to smul (#7888)
* Allows `@[to_additive]` to reorder consecutive arguments of specified identifiers.
* This can be specified with the attribute `@[to_additive_reorder n m ...]` to swap arguments `n` and `n+1`, arguments `m` and `m+1` etc. (start counting from 1).
* The only two attributes currently in use are:
```lean
attribute [to_additive_reorder 1] has_pow
attribute [to_additive_reorder 1 4] has_pow.pow
```
* It will eta-expand all expressions that have as head a declaration with attribute `to_additive_reorder` until they have the required number of arguments. This is required to correctly deal with partially applied terms.
* Hack: if the first two arguments are reordered, then the first two universe variables are also reordered (this happens to be the correct behavior for `has_pow` and `has_pow.pow`). It might be cleaner to have a separate attribute for that, but that given the low amount of times that I expect that we use `to_additive_reorder`, this seems unnecessary.
* This PR also allows the user to write `@[to_additive?]` to trace the generated declaration.
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
