From de47c4e96bcafb1d540d0334b85c1a8677931a97 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 24 Mar 2017 14:38:31 -0400 Subject: Add lemmas needed for saturated arithmetic [compact] --- src/Util/ZUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util/ZUtil.v') 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. -- cgit v1.2.3