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 **)
let rec z_rect_Type4 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4786 -> h_pos x_4786
| Neg x_4787 -> h_neg x_4787

(** val z_rect_Type5 :
    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
let rec z_rect_Type5 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4792 -> h_pos x_4792
| Neg x_4793 -> h_neg x_4793

(** val z_rect_Type3 :
    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
let rec z_rect_Type3 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4798 -> h_pos x_4798
| Neg x_4799 -> h_neg x_4799

(** val z_rect_Type2 :
    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
let rec z_rect_Type2 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4804 -> h_pos x_4804
| Neg x_4805 -> h_neg x_4805

(** val z_rect_Type1 :
    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
let rec z_rect_Type1 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4810 -> h_pos x_4810
| Neg x_4811 -> h_neg x_4811

(** val z_rect_Type0 :
    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
let rec z_rect_Type0 h_OZ h_pos h_neg = function
| OZ -> h_OZ
| Pos x_4816 -> h_pos x_4816
| Neg x_4817 -> h_neg x_4817

(** val z_inv_rect_Type4 :
    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
    'a1) -> 'a1 **)
let z_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = z_rect_Type4 h1 h2 h3 hterm in hcut __

(** val z_inv_rect_Type3 :
    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
    'a1) -> 'a1 **)
let z_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = z_rect_Type3 h1 h2 h3 hterm in hcut __

(** val z_inv_rect_Type2 :
    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
    'a1) -> 'a1 **)
let z_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = z_rect_Type2 h1 h2 h3 hterm in hcut __

(** val z_inv_rect_Type1 :
    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
    'a1) -> 'a1 **)
let z_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = z_rect_Type1 h1 h2 h3 hterm in hcut __

(** val z_inv_rect_Type0 :
    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
    'a1) -> 'a1 **)
let z_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = z_rect_Type0 h1 h2 h3 hterm in hcut __

(** val z_discr : z -> z -> __ **)
let z_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | OZ -> Obj.magic (fun _ dH -> dH)
     | Pos a0 -> Obj.magic (fun _ dH -> dH __)
     | Neg a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val z_of_nat : Nat.nat -> z **)
let z_of_nat = function
| Nat.O -> OZ
| Nat.S n0 -> Pos (Positive.succ_pos_of_nat n0)

(** val neg_Z_of_nat : Nat.nat -> z **)
let neg_Z_of_nat = function
| Nat.O -> OZ
| Nat.S n0 -> Neg (Positive.succ_pos_of_nat n0)

(** val abs : z -> Nat.nat **)
let abs = function
| OZ -> Nat.O
| Pos n -> Positive.nat_of_pos n
| Neg n -> Positive.nat_of_pos n

(** val oZ_test : z -> Bool.bool **)
let oZ_test = function
| OZ -> Bool.True
| Pos x -> Bool.False
| Neg x -> Bool.False

(** val zsucc : z -> z **)
let zsucc = function
| OZ -> Pos Positive.One
| Pos n -> Pos (Positive.succ n)
| Neg n ->
  (match n with
   | Positive.One -> OZ
   | Positive.P1 x -> Neg (Positive.pred n)
   | Positive.P0 x -> Neg (Positive.pred n))

(** val zpred : z -> z **)
let zpred = function
| OZ -> Neg Positive.One
| Pos n ->
  (match n with
   | Positive.One -> OZ
   | Positive.P1 x -> Pos (Positive.pred n)
   | Positive.P0 x -> Pos (Positive.pred n))
| Neg n -> Neg (Positive.succ n)

(** val eqZb : z -> z -> Bool.bool **)
let rec eqZb x y =
  match x with
  | OZ ->
    (match y with
     | OZ -> Bool.True
     | Pos q -> Bool.False
     | Neg q -> Bool.False)
  | Pos p ->
    (match y with
     | OZ -> Bool.False
     | Pos q -> Positive.eqb p q
     | Neg q -> Bool.False)
  | Neg p ->
    (match y with
     | OZ -> Bool.False
     | Pos q -> Bool.False
     | Neg q -> Positive.eqb p q)

(** val z_compare : z -> z -> Positive.compare **)
let rec z_compare x y =
  match x with
  | OZ ->
    (match y with
     | OZ -> Positive.EQ
     | Pos m -> Positive.LT
     | Neg m -> Positive.GT)
  | Pos n ->
    (match y with
     | OZ -> Positive.GT
     | Pos m -> Positive.pos_compare n m
     | Neg m -> Positive.GT)
  | Neg n ->
    (match y with
     | OZ -> Positive.LT
     | Pos m -> Positive.LT
     | Neg m -> Positive.pos_compare m n)

(** val zplus : z -> z -> z **)
let rec zplus x y =
  match x with
  | OZ -> y
  | Pos m ->
    (match y with
     | OZ -> x
     | Pos n -> Pos (Positive.plus m n)
     | Neg n ->
       (match Positive.pos_compare m n with
        | Positive.LT -> Neg (Positive.minus n m)
        | Positive.EQ -> OZ
        | Positive.GT -> Pos (Positive.minus m n)))
  | Neg m ->
    (match y with
     | OZ -> x
     | Pos n ->
       (match Positive.pos_compare m n with
        | Positive.LT -> Pos (Positive.minus n m)
        | Positive.EQ -> OZ
        | Positive.GT -> Neg (Positive.minus m n))
     | Neg n -> Neg (Positive.plus m n))

(** val zopp : z -> z **)
let zopp = function
| OZ -> OZ
| Pos n -> Neg n
| Neg n -> Pos n

(** val zminus : z -> z -> z **)
let zminus x y =
  zplus x (zopp y)

(** val z_two_power_nat : Nat.nat -> z **)
let z_two_power_nat n =
  Pos (Positive.two_power_nat n)

(** val z_two_power_pos : Positive.pos -> z **)
let z_two_power_pos n =
  Pos (Positive.two_power_pos n)

(** val two_p : z -> z **)
let two_p = function
| OZ -> Pos Positive.One
| Pos p -> Pos (Positive.two_power_pos p)
| Neg x -> OZ

open Types

(** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
let decidable_eq_Z_Type z1 z2 =
  (match eqZb z1 z2 with
   | Bool.True -> (fun _ -> Types.Inl __)
   | Bool.False -> (fun _ -> Types.Inr __)) __

(** val zleb : z -> z -> Bool.bool **)
let rec zleb x y =
  match x with
  | OZ ->
    (match y with
     | OZ -> Bool.True
     | Pos m -> Bool.True
     | Neg m -> Bool.False)
  | Pos n ->
    (match y with
     | OZ -> Bool.False
     | Pos m -> Positive.leb n m
     | Neg m -> Bool.False)
  | Neg n ->
    (match y with
     | OZ -> Bool.True
     | Pos m -> Bool.True
     | Neg m -> Positive.leb m n)

(** val zltb : z -> z -> Bool.bool **)
let rec zltb x y =
  match x with
  | OZ ->
    (match y with
     | OZ -> Bool.False
     | Pos m -> Bool.True
     | Neg m -> Bool.False)
  | Pos n ->
    (match y with
     | OZ -> Bool.False
     | Pos m -> Positive.leb (Positive.succ n) m
     | Neg m -> Bool.False)
  | Neg n ->
    (match y with
     | OZ -> Bool.True
     | Pos m -> Bool.True
     | Neg m -> Positive.leb (Positive.succ m) n)

(** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let zleb_elim_Type0 n m hle hnle =
  Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __

(** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let zltb_elim_Type0 n m hlt hnlt =
  Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __

(** val z_times : z -> z -> z **)
let rec z_times x y =
  match x with
  | OZ -> OZ
  | Pos n ->
    (match y with
     | OZ -> OZ
     | Pos m -> Pos (Positive.times n m)
     | Neg m -> Neg (Positive.times n m))
  | Neg n ->
    (match y with
     | OZ -> OZ
     | Pos m -> Neg (Positive.times n m)
     | Neg m -> Pos (Positive.times n m))

(** val zmax : z -> z -> z **)
let zmax x y =
  match z_compare x y with
  | Positive.LT -> y
  | Positive.EQ -> x
  | Positive.GT -> x