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 **)
let rec nat_rect_Type4 h_O h_S = function
| O -> h_O
| S x_565 -> h_S x_565 (nat_rect_Type4 h_O h_S x_565)

(** val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
let rec nat_rect_Type3 h_O h_S = function
| O -> h_O
| S x_573 -> h_S x_573 (nat_rect_Type3 h_O h_S x_573)

(** val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
let rec nat_rect_Type2 h_O h_S = function
| O -> h_O
| S x_577 -> h_S x_577 (nat_rect_Type2 h_O h_S x_577)

(** val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
let rec nat_rect_Type1 h_O h_S = function
| O -> h_O
| S x_581 -> h_S x_581 (nat_rect_Type1 h_O h_S x_581)

(** val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
let rec nat_rect_Type0 h_O h_S = function
| O -> h_O
| S x_585 -> h_S x_585 (nat_rect_Type0 h_O h_S x_585)

(** val nat_inv_rect_Type4 :
    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let nat_inv_rect_Type4 hterm h1 h2 =
  let hcut = nat_rect_Type4 h1 h2 hterm in hcut __

(** val nat_inv_rect_Type3 :
    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let nat_inv_rect_Type3 hterm h1 h2 =
  let hcut = nat_rect_Type3 h1 h2 hterm in hcut __

(** val nat_inv_rect_Type2 :
    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let nat_inv_rect_Type2 hterm h1 h2 =
  let hcut = nat_rect_Type2 h1 h2 hterm in hcut __

(** val nat_inv_rect_Type1 :
    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let nat_inv_rect_Type1 hterm h1 h2 =
  let hcut = nat_rect_Type1 h1 h2 hterm in hcut __

(** val nat_inv_rect_Type0 :
    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let nat_inv_rect_Type0 hterm h1 h2 =
  let hcut = nat_rect_Type0 h1 h2 hterm in hcut __

(** val nat_discr : nat -> nat -> __ **)
let nat_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | O -> Obj.magic (fun _ dH -> dH)
     | S a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val pred : nat -> nat **)
let pred = function
| O -> O
| S p -> p

(** val plus : nat -> nat -> nat **)
let rec plus n m =
  match n with
  | O -> m
  | S p -> S (plus p m)

(** val times : nat -> nat -> nat **)
let rec times n m =
  match n with
  | O -> O
  | S p -> plus m (times p m)

(** val minus : nat -> nat -> nat **)
let rec minus n m =
  match n with
  | O -> O
  | S p ->
    (match m with
     | O -> S p
     | S q -> minus p q)

open Bool

(** val eqb : nat -> nat -> Bool.bool **)
let rec eqb n m =
  match n with
  | O ->
    (match m with
     | O -> Bool.True
     | S q -> Bool.False)
  | S p ->
    (match m with
     | O -> Bool.False
     | S q -> eqb p q)

(** val leb : nat -> nat -> Bool.bool **)
let rec leb n m =
  match n with
  | O -> Bool.True
  | S p ->
    (match m with
     | O -> Bool.False
     | S q -> leb p q)

(** val min : nat -> nat -> nat **)
let min n m =
  match leb n m with
  | Bool.True -> n
  | Bool.False -> m

(** val max : nat -> nat -> nat **)
let max n m =
  match leb n m with
  | Bool.True -> m
  | Bool.False -> n