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.