Associativity of the tail recursively defined addition

Fixpoint plus'' (n m:nat) {struct m} : nat :=
  match m with 0 =>  n 
      | S p => plus'' (S n) p 
  end.

Solution