sig
  exception Overflow
  type nat = Big_int.big_int
  val two : CoqNat.nat
  val succ : CoqNat.nat -> CoqNat.nat
  val pred : CoqNat.nat -> CoqNat.nat
  val plus : CoqNat.nat -> CoqNat.nat -> CoqNat.nat
  val minus : CoqNat.nat -> CoqNat.nat -> CoqNat.nat
  val times : CoqNat.nat -> CoqNat.nat -> CoqNat.nat
  val eq_nat_dec : CoqNat.nat -> CoqNat.nat -> bool
  val of_int : int -> CoqNat.nat
  val of_string : string -> CoqNat.nat
end