Equality on nat is decideable

Consider the following definition:

Definition eqdec (A:Set) := forall a b : A, {a = b}+{a <> b}.

Build a certified function of the following type:

Definition nat_eq_dec : eqdec nat.

Solution