Using pattern and rewrite

Prove the following result :
Theorem plus_permute2 :
    forall n m p:nat, n + m + p = n + p + m.
Your are not allowed to use sophisticated tactics for arithmetic in this exercise. You may use rewrite, pattern, and reflexivity, as well as the following theorems of the Arith library :
plus_comm  : forall n m:nat, n + m = m + n

plus_assoc_r : forall n m p:nat, n + m + p = n + (m + p)

Solution

Look at this file