mathlib3

f13ee544 - chore(*): sort out some to_additive and simp orderings (#13038)

chore(*): sort out some to_additive and simp orderings (#13038) - To additive should always come after simp, unless the linter complains. - Also make to_additive transfer the `protected` attribute for consistency.