Properties of addition.
This file is mostly OBSOLETE now, see module
PeanoNat.Nat instead.
Nat.add is defined in
Init/Nat.v as:
Fixpoint add (n m:nat) : nat :=
match n with
| O => m
| S p => S (p + m)
end
where "n + m" := (add n m) : nat_scope.
Tail-recursive plus
tail_plus is an alternative definition for
plus which is
tail-recursive, whereas
plus is not. This can be useful
when extracting programs.