]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/primes1.ma
fix
[helm.git] / helm / matita / library / nat / primes1.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/primes1".
16
17 include "datatypes/constructors.ma".
18 include "nat/primes.ma".
19
20 (* p is just an upper bound, acc is an accumulator *)
21 let rec n_divides_aux p n m acc \def
22   match n \mod m with
23   [ O \Rightarrow 
24     match p with
25       [ O \Rightarrow pair nat nat acc n
26       | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
27   | (S a) \Rightarrow pair nat nat acc n].
28
29 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
30 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
31
32 (*
33 theorem n_divides_to_Prop: \forall n,m,p,a. 
34   match n_divides_aux p n m a with
35   [ (pair q r) \Rightarrow n = m \sup a *r].
36 intros.
37 apply nat_case (n \mod m). *)
38