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

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

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

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

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

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

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

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

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

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

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

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

val nat_compared_discr :
  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __

val nat_compared_jmdiscr :
  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __

val nat_compare : Nat.nat -> Nat.nat -> nat_compared

val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum