source: extracted/div_and_mod.ml @ 2746

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 **)
let rec mod_aux p m n =
  match p with
  | Nat.O -> m
  | Nat.S q ->
    (match Nat.leb m n with
     | Bool.True -> m
     | Bool.False -> mod_aux q (Nat.minus m (Nat.S n)) n)

(** val mod0 : Nat.nat -> Nat.nat -> Nat.nat **)
let mod0 n = function
| Nat.O -> n
| Nat.S p -> mod_aux n n p

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

(** val div : Nat.nat -> Nat.nat -> Nat.nat **)
let div n = function
| Nat.O -> Nat.S n
| Nat.S p -> div_aux n n p

(** val div_mod_spec_rect_Type4 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type4 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_rect_Type5 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type5 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_rect_Type3 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type3 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_rect_Type2 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type2 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_rect_Type1 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type1 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_rect_Type0 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
let rec div_mod_spec_rect_Type0 n m q r h_div_mod_spec_intro =
  h_div_mod_spec_intro __ __

(** val div_mod_spec_inv_rect_Type4 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let div_mod_spec_inv_rect_Type4 x1 x2 x3 x4 h1 =
  let hcut = div_mod_spec_rect_Type4 x1 x2 x3 x4 h1 in hcut __

(** val div_mod_spec_inv_rect_Type3 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let div_mod_spec_inv_rect_Type3 x1 x2 x3 x4 h1 =
  let hcut = div_mod_spec_rect_Type3 x1 x2 x3 x4 h1 in hcut __

(** val div_mod_spec_inv_rect_Type2 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let div_mod_spec_inv_rect_Type2 x1 x2 x3 x4 h1 =
  let hcut = div_mod_spec_rect_Type2 x1 x2 x3 x4 h1 in hcut __

(** val div_mod_spec_inv_rect_Type1 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let div_mod_spec_inv_rect_Type1 x1 x2 x3 x4 h1 =
  let hcut = div_mod_spec_rect_Type1 x1 x2 x3 x4 h1 in hcut __

(** val div_mod_spec_inv_rect_Type0 :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let div_mod_spec_inv_rect_Type0 x1 x2 x3 x4 h1 =
  let hcut = div_mod_spec_rect_Type0 x1 x2 x3 x4 h1 in hcut __

(** val div_mod_spec_discr :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __ **)
let div_mod_spec_discr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __