open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

type z =
| OZ
| Pos of Positive.pos
| Neg of Positive.pos

val z_rect_Type4 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_rect_Type5 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_rect_Type3 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_rect_Type2 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_rect_Type1 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_rect_Type0 :
  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1

val z_inv_rect_Type4 :
  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  'a1) -> 'a1

val z_inv_rect_Type3 :
  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  'a1) -> 'a1

val z_inv_rect_Type2 :
  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  'a1) -> 'a1

val z_inv_rect_Type1 :
  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  'a1) -> 'a1

val z_inv_rect_Type0 :
  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  'a1) -> 'a1

val z_discr : z -> z -> __

val z_of_nat : Nat.nat -> z

val neg_Z_of_nat : Nat.nat -> z

val abs : z -> Nat.nat

val oZ_test : z -> Bool.bool

val zsucc : z -> z

val zpred : z -> z

val eqZb : z -> z -> Bool.bool

val z_compare : z -> z -> Positive.compare

val zplus : z -> z -> z

val zopp : z -> z

val zminus : z -> z -> z

val z_two_power_nat : Nat.nat -> z

val z_two_power_pos : Positive.pos -> z

val two_p : z -> z

open Types

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

val zleb : z -> z -> Bool.bool

val zltb : z -> z -> Bool.bool

val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val z_times : z -> z -> z

val zmax : z -> z -> z