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