diff options
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 3 insertions, 0 deletions
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. |