ocaml 3.09 transition

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

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 7681f191f7998e1f38f62bc7ab02251cfd5a5a89..af744cf3475087290d2100638f3a6af3b729c732 100644 (file)
--- 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.