sig
  type z = Big_int.big_int
  val xO : CoqZ.z -> CoqZ.z
  val xI : CoqZ.z -> CoqZ.z
  val plus : CoqZ.z -> CoqZ.z -> CoqZ.z
  val minus : CoqZ.z -> CoqZ.z -> CoqZ.z
  val times : CoqZ.z -> CoqZ.z -> CoqZ.z
  val div : CoqZ.z -> CoqZ.z -> CoqZ.z
  val neg : CoqZ.z -> CoqZ.z
end