open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

(** val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option **)
let rec nat_bound_opt n n0 =
  match n with
  | Nat.O -> Types.None
  | Nat.S n' ->
    (match n0 with
     | Nat.O -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) __)
     | Nat.S n'0 ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Option.option)
           (Obj.magic (nat_bound_opt n' n'0)) (fun _ ->
           Monad.m_return0 (Monad.max_def Option.option) __)))

type nat_compared =
| Nat_lt of Nat.nat * Nat.nat
| Nat_eq of Nat.nat
| Nat_gt of Nat.nat * Nat.nat

(** val nat_compared_rect_Type4 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1125 x_1124 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_rect_Type5 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1131 x_1130 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_rect_Type3 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1137 x_1136 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_rect_Type2 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1143 x_1142 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_rect_Type1 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1149 x_1148 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_rect_Type0 :
    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1155 x_1154 = function
| Nat_lt (n, m) -> h_nat_lt n m
| Nat_eq n -> h_nat_eq n
| Nat_gt (n, m) -> h_nat_gt n m

(** val nat_compared_inv_rect_Type4 :
    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
  let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __ __

(** val nat_compared_inv_rect_Type3 :
    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
  let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __ __

(** val nat_compared_inv_rect_Type2 :
    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
  let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __ __

(** val nat_compared_inv_rect_Type1 :
    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
  let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __ __

(** val nat_compared_inv_rect_Type0 :
    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
  let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __ __

(** val nat_compared_discr :
    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
let nat_compared_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val nat_compared_jmdiscr :
    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
let nat_compared_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val nat_compare : Nat.nat -> Nat.nat -> nat_compared **)
let rec nat_compare n m =
  match n with
  | Nat.O ->
    (match m with
     | Nat.O -> Nat_eq Nat.O
     | Nat.S m' -> Nat_lt (Nat.O, m'))
  | Nat.S n' ->
    (match m with
     | Nat.O -> Nat_gt (n', Nat.O)
     | Nat.S m' ->
       (match nat_compare n' m' with
        | Nat_lt (x, y) -> Nat_lt ((Nat.S x), y)
        | Nat_eq x -> Nat_eq (Nat.S x)
        | Nat_gt (x, y) -> Nat_gt (x, (Nat.S y))))

(** val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum **)
let rec eq_nat_dec n m =
  match n with
  | Nat.O ->
    (match m with
     | Nat.O -> Types.Inl __
     | Nat.S m' -> Types.Inr __)
  | Nat.S n' ->
    (match m with
     | Nat.O -> Types.Inr __
     | Nat.S m' ->
       (match eq_nat_dec n' m' with
        | Types.Inl _ -> Types.Inl __
        | Types.Inr _ -> Types.Inr __))