diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-03-24 14:38:31 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-03-24 14:41:45 -0400 |
| commit | de47c4e96bcafb1d540d0334b85c1a8677931a97 (patch) | |
| tree | da9e85c9963225b0e780e0f0f9d000fda9267fb7 /src/Util/ZUtil.v | |
| parent | 834a48b306acc57eabe4cf3667cc0693ccb7983a (diff) | |
Add lemmas needed for saturated arithmetic [compact]
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. |