open Preamble

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat

val mod0 : Nat.nat -> Nat.nat -> Nat.nat

val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat

val div : Nat.nat -> Nat.nat -> Nat.nat

val div_mod_spec_rect_Type4 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_rect_Type5 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_rect_Type3 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_rect_Type2 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_rect_Type1 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_rect_Type0 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1

val div_mod_spec_inv_rect_Type4 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1

val div_mod_spec_inv_rect_Type3 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1

val div_mod_spec_inv_rect_Type2 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1

val div_mod_spec_inv_rect_Type1 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1

val div_mod_spec_inv_rect_Type0 :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1

val div_mod_spec_discr : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __