X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes1.ma;h=37fcbd21fe3b2762bae5f0f504cb58ff55918c62;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=3df3922a4887d50e19fc4ec3e0f5acfffadb2ec4;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 3df3922a4..37fcbd21f 100644
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -32,7 +32,7 @@ definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
 (*
 theorem n_divides_to_Prop: \forall n,m,p,a. 
   match n_divides_aux p n m a with
-  [ (pair q r) \Rightarrow n = (exp m a)*r].
+  [ (pair q r) \Rightarrow n = m \sup a *r].
 intros.
 apply nat_case (mod n m). *)