diff options
Diffstat (limited to 'src/Util/ZUtil/Div.v')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index a9fc4aae0..5ae17ad1a 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -258,4 +258,8 @@ Module Z. intros; subst; auto with zarith. Qed. Hint Resolve div_same' : zarith. + + Lemma div_opp_r a b : a / (-b) = ((-a) / b). + Proof. Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve div_opp_r : zarith. End Z. |