X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes1.ma;h=3ec61ee4aff75630b221cff00e359420065f6781;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=37fcbd21fe3b2762bae5f0f504cb58ff55918c62;hpb=373b88228a8f9a6b4b4dcf781bc166865f89f43d;p=helm.git

diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 37fcbd21f..3ec61ee4a 100644
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -19,11 +19,11 @@ include "nat/primes.ma".
 
 (* p is just an upper bound, acc is an accumulator *)
 let rec n_divides_aux p n m acc \def
-  match (mod n m) with
+  match n \mod m with
   [ O \Rightarrow 
     match p with
       [ O \Rightarrow pair nat nat acc n
-      | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)]
+      | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
   | (S a) \Rightarrow pair nat nat acc n].
 
 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
@@ -34,5 +34,5 @@ theorem n_divides_to_Prop: \forall n,m,p,a.
   match n_divides_aux p n m a with
   [ (pair q r) \Rightarrow n = m \sup a *r].
 intros.
-apply nat_case (mod n m). *)
+apply nat_case (n \mod m). *)