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