From 9d6c6fea193320d2a97a2b676974e9e699c9ff93 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 14:00:42 -0700 Subject: Another ZUtil lemma --- src/Util/ZUtil.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 00e227e2d..97bfd44a2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1001,6 +1001,9 @@ Module Z. intros; autorewrite with zsimplify; lia. Qed. Hint Rewrite div_sub_small using lia : zsimplify. + + Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. + Proof. lia. Qed. End Z. Module Export BoundsTactics. -- cgit v1.2.3