diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 07e9af549..38709174e 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -596,6 +596,14 @@ Module Z. Hint Rewrite mul_div_eq mul_div_eq' using zutil_arith : zdiv_to_mod. Hint Rewrite <- mul_div_eq' using zutil_arith : zmod_to_div. + Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m). + Proof. + intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. + Qed. + + Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod. + Hint Rewrite <-mul_div_eq_full using zutil_arith : zmod_to_div. + Ltac prime_bound := match goal with | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega end. |