open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Div_and_mod

(** val prodF :
    (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
    Types.prod **)
let prodF f g m x =
  { Types.fst = (f (Div_and_mod.div x m)); Types.snd =
    (g (Div_and_mod.mod0 x m)) }

(** val bigop :
    Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) ->
    (Nat.nat -> 'a1) -> 'a1 **)
let rec bigop n p nil op f =
  match n with
  | Nat.O -> nil
  | Nat.S k ->
    (match p k with
     | Bool.True -> op (f k) (bigop k p nil op f)
     | Bool.False -> bigop k p nil op f)

type 'a aop =
  'a -> 'a -> 'a
  (* singleton inductive, whose constructor was mk_Aop *)

(** val aop_rect_Type4 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type4 nil h_mk_Aop x_969 =
  let op = x_969 in h_mk_Aop op __ __ __

(** val aop_rect_Type5 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type5 nil h_mk_Aop x_971 =
  let op = x_971 in h_mk_Aop op __ __ __

(** val aop_rect_Type3 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type3 nil h_mk_Aop x_973 =
  let op = x_973 in h_mk_Aop op __ __ __

(** val aop_rect_Type2 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type2 nil h_mk_Aop x_975 =
  let op = x_975 in h_mk_Aop op __ __ __

(** val aop_rect_Type1 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type1 nil h_mk_Aop x_977 =
  let op = x_977 in h_mk_Aop op __ __ __

(** val aop_rect_Type0 :
    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
let rec aop_rect_Type0 nil h_mk_Aop x_979 =
  let op = x_979 in h_mk_Aop op __ __ __

(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
let rec op nil xxx =
  let yyy = xxx in yyy

(** val aop_inv_rect_Type4 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type4 x2 hterm h1 =
  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type3 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type3 x2 hterm h1 =
  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type2 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type2 x2 hterm h1 =
  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type1 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type1 x2 hterm h1 =
  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __

(** val aop_inv_rect_Type0 :
    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
    'a2 **)
let aop_inv_rect_Type0 x2 hterm h1 =
  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __

(** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
let aop_discr a2 x y =
  Logic.eq_rect_Type2 x
    (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val dpi1__o__op :
    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
let dpi1__o__op x1 x3 =
  op x1 x3.Types.dpi1

type 'a aCop =
  'a aop
  (* singleton inductive, whose constructor was mk_ACop *)

(** val aCop_rect_Type4 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type4 nil h_mk_ACop x_997 =
  let aop0 = x_997 in h_mk_ACop aop0 __

(** val aCop_rect_Type5 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type5 nil h_mk_ACop x_999 =
  let aop0 = x_999 in h_mk_ACop aop0 __

(** val aCop_rect_Type3 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type3 nil h_mk_ACop x_1001 =
  let aop0 = x_1001 in h_mk_ACop aop0 __

(** val aCop_rect_Type2 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type2 nil h_mk_ACop x_1003 =
  let aop0 = x_1003 in h_mk_ACop aop0 __

(** val aCop_rect_Type1 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type1 nil h_mk_ACop x_1005 =
  let aop0 = x_1005 in h_mk_ACop aop0 __

(** val aCop_rect_Type0 :
    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
let rec aCop_rect_Type0 nil h_mk_ACop x_1007 =
  let aop0 = x_1007 in h_mk_ACop aop0 __

(** val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop **)
let rec aop0 nil xxx =
  let yyy = xxx in yyy

(** val aCop_inv_rect_Type4 :
    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
let aCop_inv_rect_Type4 x2 hterm h1 =
  let hcut = aCop_rect_Type4 x2 h1 hterm in hcut __

(** val aCop_inv_rect_Type3 :
    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
let aCop_inv_rect_Type3 x2 hterm h1 =
  let hcut = aCop_rect_Type3 x2 h1 hterm in hcut __

(** val aCop_inv_rect_Type2 :
    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
let aCop_inv_rect_Type2 x2 hterm h1 =
  let hcut = aCop_rect_Type2 x2 h1 hterm in hcut __

(** val aCop_inv_rect_Type1 :
    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
let aCop_inv_rect_Type1 x2 hterm h1 =
  let hcut = aCop_rect_Type1 x2 h1 hterm in hcut __

(** val aCop_inv_rect_Type0 :
    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
let aCop_inv_rect_Type0 x2 hterm h1 =
  let hcut = aCop_rect_Type0 x2 h1 hterm in hcut __

(** val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __ **)
let aCop_discr a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__aop__o__op :
    'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
let dpi1__o__aop__o__op x1 x3 =
  op x1 (aop0 x1 x3.Types.dpi1)

(** val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1 **)
let aop__o__op x1 x2 =
  op x1 (aop0 x1 x2)

(** val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop **)
let dpi1__o__aop x1 x3 =
  aop0 x1 x3.Types.dpi1

type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
                  filter : (Nat.nat -> Bool.bool) }

(** val range_rect_Type4 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type4 h_mk_range x_1023 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1023 in
  h_mk_range enum0 upto0 filter0

(** val range_rect_Type5 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type5 h_mk_range x_1025 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1025 in
  h_mk_range enum0 upto0 filter0

(** val range_rect_Type3 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type3 h_mk_range x_1027 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1027 in
  h_mk_range enum0 upto0 filter0

(** val range_rect_Type2 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type2 h_mk_range x_1029 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1029 in
  h_mk_range enum0 upto0 filter0

(** val range_rect_Type1 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type1 h_mk_range x_1031 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1031 in
  h_mk_range enum0 upto0 filter0

(** val range_rect_Type0 :
    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
    range -> 'a2 **)
let rec range_rect_Type0 h_mk_range x_1033 =
  let { enum = enum0; upto = upto0; filter = filter0 } = x_1033 in
  h_mk_range enum0 upto0 filter0

(** val enum : 'a1 range -> Nat.nat -> 'a1 **)
let rec enum xxx =
  xxx.enum

(** val upto : 'a1 range -> Nat.nat **)
let rec upto xxx =
  xxx.upto

(** val filter : 'a1 range -> Nat.nat -> Bool.bool **)
let rec filter xxx =
  xxx.filter

(** val range_inv_rect_Type4 :
    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
    -> 'a2) -> 'a2 **)
let range_inv_rect_Type4 hterm h1 =
  let hcut = range_rect_Type4 h1 hterm in hcut __

(** val range_inv_rect_Type3 :
    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
    -> 'a2) -> 'a2 **)
let range_inv_rect_Type3 hterm h1 =
  let hcut = range_rect_Type3 h1 hterm in hcut __

(** val range_inv_rect_Type2 :
    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
    -> 'a2) -> 'a2 **)
let range_inv_rect_Type2 hterm h1 =
  let hcut = range_rect_Type2 h1 hterm in hcut __

(** val range_inv_rect_Type1 :
    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
    -> 'a2) -> 'a2 **)
let range_inv_rect_Type1 hterm h1 =
  let hcut = range_rect_Type1 h1 hterm in hcut __

(** val range_inv_rect_Type0 :
    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
    -> 'a2) -> 'a2 **)
let range_inv_rect_Type0 hterm h1 =
  let hcut = range_rect_Type0 h1 hterm in hcut __

(** val range_discr : 'a1 range -> 'a1 range -> __ **)
let range_discr x y =
  Logic.eq_rect_Type2 x
    (let { enum = a0; upto = a10; filter = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }

(** val dop_rect_Type4 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type4 nil h_mk_Dop x_1051 =
  let { sum0 = sum1; prod0 = prod1 } = x_1051 in h_mk_Dop sum1 prod1 __ __

(** val dop_rect_Type5 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type5 nil h_mk_Dop x_1053 =
  let { sum0 = sum1; prod0 = prod1 } = x_1053 in h_mk_Dop sum1 prod1 __ __

(** val dop_rect_Type3 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type3 nil h_mk_Dop x_1055 =
  let { sum0 = sum1; prod0 = prod1 } = x_1055 in h_mk_Dop sum1 prod1 __ __

(** val dop_rect_Type2 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type2 nil h_mk_Dop x_1057 =
  let { sum0 = sum1; prod0 = prod1 } = x_1057 in h_mk_Dop sum1 prod1 __ __

(** val dop_rect_Type1 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type1 nil h_mk_Dop x_1059 =
  let { sum0 = sum1; prod0 = prod1 } = x_1059 in h_mk_Dop sum1 prod1 __ __

(** val dop_rect_Type0 :
    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
    'a2 **)
let rec dop_rect_Type0 nil h_mk_Dop x_1061 =
  let { sum0 = sum1; prod0 = prod1 } = x_1061 in h_mk_Dop sum1 prod1 __ __

(** val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop **)
let rec sum0 nil xxx =
  xxx.sum0

(** val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1 **)
let rec prod0 nil xxx =
  xxx.prod0

(** val dop_inv_rect_Type4 :
    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
    'a2) -> 'a2 **)
let dop_inv_rect_Type4 x2 hterm h1 =
  let hcut = dop_rect_Type4 x2 h1 hterm in hcut __

(** val dop_inv_rect_Type3 :
    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
    'a2) -> 'a2 **)
let dop_inv_rect_Type3 x2 hterm h1 =
  let hcut = dop_rect_Type3 x2 h1 hterm in hcut __

(** val dop_inv_rect_Type2 :
    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
    'a2) -> 'a2 **)
let dop_inv_rect_Type2 x2 hterm h1 =
  let hcut = dop_rect_Type2 x2 h1 hterm in hcut __

(** val dop_inv_rect_Type1 :
    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
    'a2) -> 'a2 **)
let dop_inv_rect_Type1 x2 hterm h1 =
  let hcut = dop_rect_Type1 x2 h1 hterm in hcut __

(** val dop_inv_rect_Type0 :
    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
    'a2) -> 'a2 **)
let dop_inv_rect_Type0 x2 hterm h1 =
  let hcut = dop_rect_Type0 x2 h1 hterm in hcut __

(** val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __ **)
let dop_discr a2 x y =
  Logic.eq_rect_Type2 x
    (let { sum0 = a0; prod0 = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y