1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/primes1".
17 include "datatypes/constructors.ma".
18 include "nat/primes.ma".
21 (* p is just an upper bound, acc is an accumulator *)
22 let rec n_divides_aux p n m acc \def
26 [ O \Rightarrow pair nat nat acc n
27 | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)]
28 | (S a) \Rightarrow pair nat nat acc n].
30 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
31 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
34 theorem n_divides_to_Prop: \forall n,m,p,a.
35 match n_divides_aux p n m a with
36 [ (pair q r) \Rightarrow n = (exp m a)*r].
38 apply nat_case (mod n m). *)