From a201b0a8e525cab5c3cb019ccd707b7367aa3ecc Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 15:30:56 -0400 Subject: add some hints to the global databases --- src/Util/ZUtil/Div.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/ZUtil/Div.v') 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. -- cgit v1.2.3