Another definition of addition

Give a definition of addition on nat, recursive on its second argument (and not the first one, as plus).
Prove that your functions computes the same result as Coq's plus.

Solution

Look at this file

Going home

Pierre Castéran