open Preamble

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

type natp =
| Pzero
| Ppos of Positive.pos

val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1

val natp_inv_rect_Type4 :
  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1

val natp_inv_rect_Type3 :
  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1

val natp_inv_rect_Type2 :
  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1

val natp_inv_rect_Type1 :
  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1

val natp_inv_rect_Type0 :
  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1

val natp_discr : natp -> natp -> __

val natp0 : natp -> natp

val natp1 : natp -> natp

val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod

val div : Positive.pos -> Positive.pos -> natp

val mod0 : Positive.pos -> Positive.pos -> natp

val natp_plus : natp -> natp -> natp

val natp_times : natp -> natp -> natp

val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum

val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum

val natp_to_Z : natp -> Z.z

val natp_to_negZ : natp -> Z.z

val divZ : Z.z -> Z.z -> Z.z

val modZ : Z.z -> Z.z -> Z.z