Module Micromega.Coq_Pos

val succ : positive -> positive
val add : positive -> positive -> positive
val add_carry : positive -> positive -> positive
val pred_double : positive -> positive
type mask = Pos.mask =
| IsNul
| IsPos of positive
| IsNeg
val succ_double_mask : mask -> mask
val double_mask : mask -> mask
val double_pred_mask : positive -> mask
val sub_mask : positive -> positive -> mask
val sub_mask_carry : positive -> positive -> mask
val sub : positive -> positive -> positive
val mul : positive -> positive -> positive
val size_nat : positive -> nat
val compare_cont : comparison -> positive -> positive -> comparison
val compare : positive -> positive -> comparison
val gcdn : nat -> positive -> positive -> positive
val gcd : positive -> positive -> positive
val of_succ_nat : nat -> positive