extracted/div_and_mod.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
  18
  19 val mod0 : Nat.nat -> Nat.nat -> Nat.nat
  20
  21 val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
  22
  23 val div : Nat.nat -> Nat.nat -> Nat.nat
  24
  25 val div_mod_spec_rect_Type4 :
  26   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  27
  28 val div_mod_spec_rect_Type5 :
  29   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  30
  31 val div_mod_spec_rect_Type3 :
  32   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  33
  34 val div_mod_spec_rect_Type2 :
  35   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  36
  37 val div_mod_spec_rect_Type1 :
  38   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  39
  40 val div_mod_spec_rect_Type0 :
  41   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
  42
  43 val div_mod_spec_inv_rect_Type4 :
  44   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
  45
  46 val div_mod_spec_inv_rect_Type3 :
  47   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
  48
  49 val div_mod_spec_inv_rect_Type2 :
  50   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
  51
  52 val div_mod_spec_inv_rect_Type1 :
  53   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
  54
  55 val div_mod_spec_inv_rect_Type0 :
  56   Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
  57
  58 val div_mod_spec_discr : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __
  59