diff options
| -rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 64604022a..2d3f24c07 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2566,6 +2566,13 @@ Module Z. | [ |- context[(?a mod ?n) mod ?m] ] => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver end. + Ltac rewrite_mod_mod_small := + repeat match goal with + | [ |- context[(?a mod ?n) mod ?m] ] + => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver + end. + Ltac rewrite_mod_small_more := + repeat (rewrite_mod_small || rewrite_mod_mod_small). Local Ltac simplify_div_tac := intros; autorewrite with zsimplify; rewrite <- ?Z_div_plus_full_l, <- ?Z_div_plus_full by assumption; |