diff options
Diffstat (limited to 'src/Util/ZUtil/Div.v')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 7012f83c0..4995ba76b 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -45,10 +45,10 @@ Module Z. Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. - Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. - + Hint Rewrite Z.div_add' Z.div_add_l' using zutil_arith : push_Zdiv. + Hint Rewrite <- Z.div_add' Z.div_add_l' using zutil_arith : pull_Zdiv. Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify. Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b. |