feat(simps): interaction between simps and to_additive (#5331)
If a definition is both marked `to_additive` and `simps` (in that order), `simps` will from also apply the `to_additive` attribute to its generated lemmas (which creates the additive counterparts of the simp-lemmas).
This also generalizes `set_attribute` to use the default parameter if possible.
This implements half of #1639.
