A direct definition of addition

Give another definition of addition on nat, without using Fixpoint nor fix, but as an application of nat_rec.
Is your definition equivalent to Coq's plus ?

Solution

Look at this file


Going home
Pierre Castéran