why is mul_assoc not mul_assoc.symm?

Stream: general

[Kevin Buzzard]

I think I've asked this before, but I didn't understand the answer. As far as I can see, a * b * c is simpler than a * (b * c), so why isn't mul_assoc.symm a simp lemma, sending (a * b) * c to a * b * c, and then we could have simp lemmas like a * b * b\-1 = a and a * b\-1 * b = a and get a confluent rewriting system for groups which doesn't have a normal form with a gazillion brackets in?