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 function computes the same result as
Coq
's
plus
.
Solution
Look at
this file