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)