let nat_of_int =
  let rec f = function n -> (* n >= 0 *)
                            if n = 0 then zero ()
                                     else suc (f (n - 1))
in
  function
    z -> if z >= 0
           then f (z)
           else failwith ("nat_of_int : requires a non-negative integer as its argument")