val double : z -> z
val succ_double : z -> z
val pred_double : z -> z
val pos_sub : positive -> positive -> z
val add : z -> z -> z
val opp : z -> z
val sub : z -> z -> z
val mul : z -> z -> z
val pow_pos : z -> positive -> z
val pow : z -> z -> z
val compare : z -> z -> comparison
val leb : z -> z -> bool
val ltb : z -> z -> bool
val gtb : z -> z -> bool
val max : z -> z -> z
val abs : z -> z
val to_N : z -> n
val of_nat : nat -> z
val of_N : n -> z
val pos_div_eucl : positive -> z -> z * z
val div_eucl : z -> z -> z * z
val div : z -> z -> z
val gcd : z -> z -> z