tactic for specificed commutativity and associativity?

Stream: Is there code for X?

[Sigma]

I was wondering if there was some method to prove ac_refl like theorems where the operation isn't commutative, but the only things we care about moving commute. Im trying to show some rearrangement of 6 terms in a ring, and the only thing I want to move are integer coerced values.
Or do I just need to bite the bullet and make a calc

[Alex J. Best]

I don't know a tactic that will do such goals for you, but tactic#assoc_rw can be helpful in these situations, maybe you can use it to more easily collect all the integers on one side.
Alternatively a well chosen simp only [add_assoc, mul_coe, \<- coe_mul] type call might normalize things for you? With mul_coe being an imaginary lemma that says coercions of integers commute with other values

[Alex J. Best]

If you provide an example of the sort of goal you are looking at maybe people will have better suggestions