Require Import Arith ZArith List Bool Psatz.

(* Define a function that has the following type
   forall x y : nat, {z | z = x + y}
   and whose algorithmic content is the same as function add'
   from file exercise3.v *)