*** empty log message ***

[helm.git] / helm / matita / library / nat / primes1.ma

diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 55d643262e15b4d4201359a0a6f0c01d515c9871..37fcbd21fe3b2762bae5f0f504cb58ff55918c62 100644 (file)
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/primes1".
 
 include "datatypes/constructors.ma".
 include "nat/primes.ma".
-include "nat/exp.ma".
 
 (* p is just an upper bound, acc is an accumulator *)
 let rec n_divides_aux p n m acc \def
@@ -33,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). *)