3 (function p -> (function m -> (function n ->
4 (match (Matita_nat_compare.leb m n) with
5 Matita_datatypes_bool.True -> m
6 | Matita_datatypes_bool.False ->
9 | Matita_nat_nat.S(q) -> (mod_aux q (Matita_nat_minus.minus m (Matita_nat_nat.S(n))) n))
15 (function n -> (function m ->
18 | Matita_nat_nat.S(p) -> (mod_aux n n p))
24 (function p -> (function m -> (function n ->
25 (match (Matita_nat_compare.leb m n) with
26 Matita_datatypes_bool.True -> Matita_nat_nat.O
27 | Matita_datatypes_bool.False ->
29 Matita_nat_nat.O -> Matita_nat_nat.O
30 | Matita_nat_nat.S(q) -> (Matita_nat_nat.S((div_aux q (Matita_nat_minus.minus m (Matita_nat_nat.S(n))) n))))
36 (function n -> (function m ->
38 Matita_nat_nat.O -> (Matita_nat_nat.S(n))
39 | Matita_nat_nat.S(p) -> (div_aux n n p))
43 let div_mod_spec_rec =
44 (function n -> (function n1 -> (function n2 -> (function n3 -> (function f -> (f))))))
47 let div_mod_spec_rect =
48 (function n -> (function n1 -> (function n2 -> (function n3 -> (function f -> (f))))))
52 let rec n_divides_aux =
53 (function p -> (function n -> (function m -> (function acc ->
54 (match (mod_ n m) with
57 Matita_nat_nat.O -> (Matita_datatypes_constructors.Pair(acc,n))
58 | Matita_nat_nat.S(p) -> (n_divides_aux p (div n m) m (Matita_nat_nat.S(acc))))
60 | Matita_nat_nat.S(a) -> (Matita_datatypes_constructors.Pair(acc,n)))
65 (function n -> (function m -> (n_divides_aux n n m Matita_nat_nat.O)))