open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Bool

open Relations

open Nat

type compare =
| LT
| EQ
| GT

val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1

val compare_inv_rect_Type4 :
  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val compare_inv_rect_Type3 :
  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val compare_inv_rect_Type2 :
  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val compare_inv_rect_Type1 :
  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val compare_inv_rect_Type0 :
  compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val compare_discr : compare -> compare -> __

val compare_invert : compare -> compare

type pos =
| One
| P1 of pos
| P0 of pos

val pos_rect_Type4 :
  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1

val pos_rect_Type3 :
  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1

val pos_rect_Type2 :
  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1

val pos_rect_Type1 :
  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1

val pos_rect_Type0 :
  'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1

val pos_inv_rect_Type4 :
  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  'a1) -> __ -> 'a1) -> 'a1

val pos_inv_rect_Type3 :
  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  'a1) -> __ -> 'a1) -> 'a1

val pos_inv_rect_Type2 :
  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  'a1) -> __ -> 'a1) -> 'a1

val pos_inv_rect_Type1 :
  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  'a1) -> __ -> 'a1) -> 'a1

val pos_inv_rect_Type0 :
  pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
  'a1) -> __ -> 'a1) -> 'a1

val pos_discr : pos -> pos -> __

val pred : pos -> pos

val succ : pos -> pos

val nat_of_pos : pos -> Nat.nat

val succ_pos_of_nat : Nat.nat -> pos

val plus : pos -> pos -> pos

val times : pos -> pos -> pos

type minusresult =
| MinusNeg
| MinusZero
| MinusPos of pos

val minusresult_rect_Type4 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_rect_Type5 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_rect_Type3 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_rect_Type2 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_rect_Type1 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_rect_Type0 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1

val minusresult_inv_rect_Type4 :
  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1

val minusresult_inv_rect_Type3 :
  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1

val minusresult_inv_rect_Type2 :
  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1

val minusresult_inv_rect_Type1 :
  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1

val minusresult_inv_rect_Type0 :
  minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1

val minusresult_discr : minusresult -> minusresult -> __

val partial_minus : pos -> pos -> minusresult

val minus : pos -> pos -> pos

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

val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

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

val pos_compare : pos -> pos -> compare

val two_power_nat : Nat.nat -> pos

val two_power_pos : pos -> pos

val max : pos -> pos -> pos