feat(attribute/to_additive): apply to_additive recursively

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[cipher1024]

@digama0, @johoelzl: any thoughts?

[johoelzl]

This looks great!

[robertylewis]

There are conflicts here now, but I think this should be mergeable when those are fixed.

[cipher1024]

Actually, I put this PR on hold as I looked at other projects. There's something broken about the way I put this into application. I'm going to try to make it work today.

[robertylewis]

@cipher1024 This is from October and has various conflicts. Can we close and reopen if/when you come back to it?

[cipher1024]

Ok, sure