how to rearrange terms in Coq using plus communtativity and associativity?

I have a general question about how to rearrange terms in Coq. For example, if we have a term m + p + n + p, humans can quickly re-arrange the terms to something like m + n + p + p (implicitly using plus_comm and plus_assoc). How do we do this efficiently in Coq?

For a (silly) example,

Require Import Coq.Arith.Plus.
Require Import Coq.Setoids.Setoid.

Theorem plus_comm_test: forall n m p: nat,
  m + p + (n + p) = m + n + 2 * p.
Proof. intros. rewrite plus_assoc. simpl. rewrite <- plus_n_O.

Now, we have

1 subgoals
...
______________________________________(1/1)
m + p + n + p = m + n + (p + p)

My question is:

How do I rewrite the LHS to m + n + p + p effectively?

I tried to use rewrite plus_comm at 2, but it gives an error Nothing to rewrite. Simply using rewrite plus_comm changes the LHS to p + m + n + p.

Any suggestions on effective rewrites are also welcome.

Thanks.

Solution

As Arthur says sometimes omega is not enough, but I sometimes use it for simple steps like this.

Require Import Omega.
Theorem test: forall a b c:nat, a + b + 2 * c = c + b + a + c.
  intros.
  replace (c + b + a) with (a + b + c) by omega.
  replace (a + b + c + c) with (a + b + (c + c)) by omega.
  replace (c + c) with (2 * c) by omega.
  reflexivity.
Qed.

This is a silly example, because omega would have solved it all in one go, but sometimes you want to rewrite things inside functions that omega can't reach into without a little help...