X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ffactorization.ma;h=92f64e56d9a9c7a556a21f1cacd6d60edaf3b81e;hb=a57ca0d68754b946b33976acf2e72f45ff11c8d7;hp=6226f3b6de81997ac3eefa61006d0c54205deafc;hpb=37f225a76270658463fb28f9d2619efcecabdcd2;p=helm.git

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 6226f3b6d..92f64e56d 100644
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -526,7 +526,7 @@ split
       [apply lt_O_nth_prime_n
       |apply (lt_O_n_elim ? H).
        intro.
-       apply (witness ? ? (r*(nth_prime p \sup m))).
+       apply (witness ? ? ((r*(nth_prime p) \sup m))).
        rewrite < assoc_times.
        rewrite < sym_times in \vdash (? ? ? (? % ?)).
        rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).