N_as_OT (djot.Djot_kernel.OrdersEx.N_as

val succ_double : BinNums.coq_N -> BinNums.coq_N

val double : BinNums.coq_N -> BinNums.coq_N

val succ_pos : BinNums.coq_N -> BinNums.positive

val sub : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

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

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

val pos_div_eucl : 
  BinNums.positive ->
  BinNums.coq_N ->
  BinNums.coq_N * BinNums.coq_N

val coq_lor : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val coq_land : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val ldiff : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val coq_lxor : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

type t = BinNums.coq_N

val zero : BinNums.coq_N

val one : BinNums.coq_N

val two : BinNums.coq_N

val succ : BinNums.coq_N -> BinNums.coq_N

val pred : BinNums.coq_N -> BinNums.coq_N

val add : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val mul : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

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

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

val min : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val max : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val div2 : BinNums.coq_N -> BinNums.coq_N

val even : BinNums.coq_N -> bool

val odd : BinNums.coq_N -> bool

val pow : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val square : BinNums.coq_N -> BinNums.coq_N

val log2 : BinNums.coq_N -> BinNums.coq_N

val size : BinNums.coq_N -> BinNums.coq_N

val size_nat : BinNums.coq_N -> int

val div_eucl : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N * BinNums.coq_N

val div : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val modulo : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val gcd : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val ggcd : 
  BinNums.coq_N ->
  BinNums.coq_N ->
  BinNums.coq_N * (BinNums.coq_N * BinNums.coq_N)

val sqrtrem : BinNums.coq_N -> BinNums.coq_N * BinNums.coq_N

val sqrt : BinNums.coq_N -> BinNums.coq_N

val shiftl_nat : BinNums.coq_N -> int -> BinNums.coq_N

val shiftr_nat : BinNums.coq_N -> int -> BinNums.coq_N

val shiftl : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val shiftr : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val testbit_nat : BinNums.coq_N -> int -> bool

val testbit : BinNums.coq_N -> BinNums.coq_N -> bool

val to_nat : BinNums.coq_N -> int

val of_nat : int -> BinNums.coq_N

val iter : BinNums.coq_N -> ('a1 -> 'a1) -> 'a1 -> 'a1

val of_uint : Decimal.uint -> BinNums.coq_N

val of_hex_uint : Hexadecimal.uint -> BinNums.coq_N

val of_num_uint : Number.uint -> BinNums.coq_N

val of_int : Decimal.signed_int -> BinNums.coq_N option

val of_hex_int : Hexadecimal.signed_int -> BinNums.coq_N option

val of_num_int : Number.signed_int -> BinNums.coq_N option

val to_uint : BinNums.coq_N -> Decimal.uint

val to_hex_uint : BinNums.coq_N -> Hexadecimal.uint

val to_num_uint : BinNums.coq_N -> Number.uint

val to_num_hex_uint : BinNums.coq_N -> Number.uint

val to_int : BinNums.coq_N -> Decimal.signed_int

val to_hex_int : BinNums.coq_N -> Hexadecimal.signed_int

val to_num_int : BinNums.coq_N -> Number.signed_int

val to_num_hex_int : BinNums.coq_N -> Number.signed_int

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

val discr : BinNums.coq_N -> BinNums.positive option

val binary_rect : 
  'a1 ->
  (BinNums.coq_N -> 'a1 -> 'a1) ->
  (BinNums.coq_N -> 'a1 -> 'a1) ->
  BinNums.coq_N ->
  'a1

val binary_rec : 
  'a1 ->
  (BinNums.coq_N -> 'a1 -> 'a1) ->
  (BinNums.coq_N -> 'a1 -> 'a1) ->
  BinNums.coq_N ->
  'a1

val peano_rect : 'a1 -> (BinNums.coq_N -> 'a1 -> 'a1) -> BinNums.coq_N -> 'a1

val peano_rec : 'a1 -> (BinNums.coq_N -> 'a1 -> 'a1) -> BinNums.coq_N -> 'a1

val recursion : 'a1 -> (BinNums.coq_N -> 'a1 -> 'a1) -> BinNums.coq_N -> 'a1

val leb_spec0 : BinNums.coq_N -> BinNums.coq_N -> Datatypes.reflect

val ltb_spec0 : BinNums.coq_N -> BinNums.coq_N -> Datatypes.reflect

module Private_OrderTac : sig ... end

val measure_right_induction : 
  ('a1 -> BinNums.coq_N) ->
  BinNums.coq_N ->
  ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) ->
  'a1 ->
  'a2

val measure_left_induction : 
  ('a1 -> BinNums.coq_N) ->
  BinNums.coq_N ->
  ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) ->
  'a1 ->
  'a2

val measure_induction : 
  ('a1 -> BinNums.coq_N) ->
  ('a1 -> ('a1 -> __ -> 'a2) -> 'a2) ->
  'a1 ->
  'a2

module Private_Tac : sig ... end

module Private_Dec : sig ... end

val max_case_strong : 
  BinNums.coq_N ->
  BinNums.coq_N ->
  (__ -> 'a1) ->
  (__ -> 'a1) ->
  'a1

val max_case : BinNums.coq_N -> BinNums.coq_N -> 'a1 -> 'a1 -> 'a1

val max_dec : BinNums.coq_N -> BinNums.coq_N -> bool

val min_case_strong : 
  BinNums.coq_N ->
  BinNums.coq_N ->
  (__ -> 'a1) ->
  (__ -> 'a1) ->
  'a1

val min_case : BinNums.coq_N -> BinNums.coq_N -> 'a1 -> 'a1 -> 'a1

val min_dec : BinNums.coq_N -> BinNums.coq_N -> bool

module Private_NZPow : sig ... end

module Private_NZSqrt : sig ... end

val sqrt_up : BinNums.coq_N -> BinNums.coq_N

val log2_up : BinNums.coq_N -> BinNums.coq_N

module Private_NZGcdProp : sig ... end

module Private_NDivProp : sig ... end

module Div0 : sig ... end

module Private_NLcmProp : sig ... end

val lcm : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

module Lcm0 : sig ... end

val eqb_spec : BinNums.coq_N -> BinNums.coq_N -> Datatypes.reflect

val b2n : bool -> BinNums.coq_N

val setbit : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val clearbit : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N

val ones : BinNums.coq_N -> BinNums.coq_N

val lnot : BinNums.coq_N -> BinNums.coq_N -> BinNums.coq_N