From be267954b7267b8564e4125b58349e0860f31967 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 19:24:51 -0700 Subject: Add ZUtil hints --- src/Util/ZUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/ZUtil.v') 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) <= -- cgit v1.2.3