Z (djot.Djot_kernel.BinInt.Z)

val double : BinNums.coq_Z -> BinNums.coq_Z

val succ_double : BinNums.coq_Z -> BinNums.coq_Z

val pred_double : BinNums.coq_Z -> BinNums.coq_Z

val pos_sub : BinNums.positive -> BinNums.positive -> BinNums.coq_Z

val add : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z

val opp : BinNums.coq_Z -> BinNums.coq_Z

val sub : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z

val mul : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z

val compare : BinNums.coq_Z -> BinNums.coq_Z -> Datatypes.comparison

val leb : BinNums.coq_Z -> BinNums.coq_Z -> bool

val ltb : BinNums.coq_Z -> BinNums.coq_Z -> bool

val eqb : BinNums.coq_Z -> BinNums.coq_Z -> bool

val max : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z

val eq_dec : BinNums.coq_Z -> BinNums.coq_Z -> bool