feat(simps): better name for additivized simps-lemmas (#8457)
* When using `@[to_additive foo, simps]`, the additivized simp-lemmas will have name `foo` + projection suffix (or prefix)
* Also add an option for `@[to_additive]` to accept the attribute with the correct given name. This is only useful when adding the `@[to_additive]` attribute via metaprogramming, so this option cannot be set by the `to_additive` argument parser.
