open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

type nat =
| O
| S of nat

val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1

val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1

val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1

val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1

val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1

val nat_inv_rect_Type4 :
  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val nat_inv_rect_Type3 :
  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val nat_inv_rect_Type2 :
  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val nat_inv_rect_Type1 :
  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val nat_inv_rect_Type0 :
  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val nat_discr : nat -> nat -> __

val pred : nat -> nat

val plus : nat -> nat -> nat

val times : nat -> nat -> nat

val minus : nat -> nat -> nat

open Bool

val eqb : nat -> nat -> Bool.bool

val leb : nat -> nat -> Bool.bool

val min : nat -> nat -> nat

val max : nat -> nat -> nat