diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-01 19:24:51 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-01 19:24:51 -0700 |
| commit | be267954b7267b8564e4125b58349e0860f31967 (patch) | |
| tree | 4bc715e0de4000f68adc3c479d0ee9d63a7da1ce /src/Util/ZUtil.v | |
| parent | d67a1312959e1ce64bcc608d0c360efc3dc6f5b3 (diff) | |
Add ZUtil hints
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 21456fea9..fe329d3f9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -612,6 +612,8 @@ Proof. pose proof (Zdiv_mul_le_le a b c); lia. Qed. +Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Zdiv_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. + (** * [Zsimplify_fractions_le] *) (** The culmination of this series of tactics, [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= |