X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcongruence.ma;h=af744cf3475087290d2100638f3a6af3b729c732;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=6bc2b6f689bc5d6266651ebc41e6c09bffeb0250;hpb=65312e560c25b49336241762107e401e7f9c5c3c;p=helm.git

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 6bc2b6f68..af744cf34 100644
--- a/helm/matita/library/nat/congruence.ma
+++ b/helm/matita/library/nat/congruence.ma
@@ -54,8 +54,8 @@ qed.
 
 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
 intros.
-apply div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p)).
+apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
+(n/(m*p)*m + (n \mod (m*p)/p))).
 apply div_mod_spec_div_mod.assumption.
 constructor 1.
 apply lt_mod_m_m.assumption.
@@ -65,7 +65,7 @@ rewrite < div_mod.
 rewrite > assoc_times.
 rewrite < div_mod.
 reflexivity.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 assumption.assumption.assumption.
 qed.