1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 045fb03a..9b8f2abb 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -406,6 +406,12 @@ Qed.
 
 (** Properties of Euclidean division and modulus. *)
 
+Lemma Z_div_mod_eq: forall a b,
+  b > 0 -> a = (b * (a / b) + a mod b).
+Proof.
+  intros. apply Z.div_mod. lia.
+Qed.
+
 Lemma Zmod_unique:
   forall x y a b,
   x = a * y + b -> 0 <= b < y -> x mod y = b.