Associativity of the tail recursively defined of 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
Going home
Pierre Castéran