newbie question

Stream: new members

[Abe Tusk]

I'm going through the 'numbers game' and I'm getting stuck on 'multiplication world' level 9 trying to prove a(bc)=b(ac). I've applied two rules:

rw mul_comm,
rw mul_assoc,

to yield b*(c*a) =b*(a*c). I would like to use mul_comm just on the c*a portion but whenever I do, it yields c*a*b=b*(a*c). Is there a way to force mul_comm to only work on the portion that I actually want?

[Kevin Buzzard]

You can do things like mul_comm a b to force it to change a * b to b * a.

[Kevin Buzzard]

Or mul_comm c to force it to change c * <something> into <something> * c

[Abe Tusk]

@Kevin Buzzard thank you!