X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcongruence.ma;h=af744cf3475087290d2100638f3a6af3b729c732;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7681f191f7998e1f38f62bc7ab02251cfd5a5a89;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 7681f191f..af744cf34 100644
--- a/helm/matita/library/nat/congruence.ma
+++ b/helm/matita/library/nat/congruence.ma
@@ -52,12 +52,36 @@ assumption.
 assumption.
 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_div_mod.assumption.
+constructor 1.
+apply lt_mod_m_m.assumption.
+rewrite > times_plus_l.
+rewrite > assoc_plus.
+rewrite < div_mod.
+rewrite > assoc_times.
+rewrite < div_mod.
+reflexivity.
+rewrite > (times_n_O O).
+apply lt_times.
+assumption.assumption.assumption.
+qed.
+
 theorem congruent_n_mod_n : 
 \forall n,p:nat. O < p \to congruent n (n \mod p) p.
 intros.unfold congruent.
 apply mod_mod.assumption.
 qed.
 
+theorem congruent_n_mod_times : 
+\forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
+intros.unfold congruent.
+apply mod_times_mod.assumption.assumption.
+qed.
+
 theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to 
 n = r*p+m \to congruent n m p.
 intros.unfold congruent.