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

Follow this link