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