diff options
| author |  jadep <jadep@mit.edu> | 2019-03-12 15:30:56 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-03-26 08:35:33 -0400 |
| commit | a201b0a8e525cab5c3cb019ccd707b7367aa3ecc (patch) | |
| tree | f53c6cdc31eb546681a5689af454f04281a9b9b6 /src/Util/ZUtil/Div.v | |
| parent | 14bd0770e068e5669cdbc4a0135e4cb65b3dad94 (diff) | |
add some hints to the global databases
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. |