Associativity of the tail recursively defined addition

Consider the following function:
Fixpoint plus'' (n m:nat) {struct m} : nat :=
  match m with 0 =>  n 
      | S p => plus'' (S n) p 
  end.
Prove that plus'' is associative.

Solution

Look at This file