Another addition function

Consider the following definition on addition:

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

Show (without using plus) that plus' is associative.

Solution