# 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