X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcongruence.ma;h=af744cf3475087290d2100638f3a6af3b729c732;hb=9ffc433e8913660620b1dd4ce4c22db1e42c7562;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
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.