17 val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
19 val mod0 : Nat.nat -> Nat.nat -> Nat.nat
21 val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
23 val div : Nat.nat -> Nat.nat -> Nat.nat
25 val div_mod_spec_rect_Type4 :
26 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
28 val div_mod_spec_rect_Type5 :
29 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
31 val div_mod_spec_rect_Type3 :
32 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
34 val div_mod_spec_rect_Type2 :
35 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
37 val div_mod_spec_rect_Type1 :
38 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
40 val div_mod_spec_rect_Type0 :
41 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
43 val div_mod_spec_inv_rect_Type4 :
44 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
46 val div_mod_spec_inv_rect_Type3 :
47 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
49 val div_mod_spec_inv_rect_Type2 :
50 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
52 val div_mod_spec_inv_rect_Type1 :
53 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
55 val div_mod_spec_inv_rect_Type0 :
56 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
58 val div_mod_spec_discr : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __