From f4f609f598fb4804acf272209782b60d4647cad4 Mon Sep 17 00:00:00 2001
From: Russell O'Connor <roconnor@blockstream.io>
Date: Thu, 29 Jun 2017 15:17:06 -0400
Subject: Add Z.mod_div lemma to standard library.

---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 8 ++++++++
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 8 ++++++++
 theories/Numbers/Integer/Abstract/ZDivTrunc.v | 8 ++++++++
 theories/ZArith/Zdiv.v                        | 6 ++++++
 4 files changed, 30 insertions(+)

(limited to 'theories')

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index c2fa69e53..c5b8d5ebe 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -602,6 +602,14 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_div: forall a b, b~=0 ->
+ a mod b / b == 0.
+Proof.
+ intros a b Hb.
+ rewrite div_small_iff by assumption.
+ auto using mod_always_pos.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 310748ddb..eeb803eea 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -650,6 +650,14 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_div: forall a b, b~=0 ->
+ a mod b / b == 0.
+Proof.
+ intros a b Hb.
+ rewrite div_small_iff by assumption.
+ auto using mod_bound_or.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 043010779..a9b72d815 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -622,6 +622,14 @@ Proof.
  apply quot_rem; order.
 Qed.
 
+Lemma rem_quot: forall a b, b~=0 ->
+ a rem b ÷ b == 0.
+Proof.
+ intros a b Hb.
+ rewrite quot_small_iff by assumption.
+ auto using rem_bound_abs.
+Qed.
+
 (** A last inequality: *)
 
 Theorem quot_mul_le:
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 2ba865bd0..509384104 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -508,6 +508,12 @@ Qed.
 (** Unfortunately, the previous result isn't always true on negative numbers.
     For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *)
 
+Lemma Zmod_div (a b : Z) : a mod b / b = 0.
+Proof.
+ zero_or_not b.
+ auto using Z.mod_div.
+Qed.
+
 (** A last inequality: *)
 
 Theorem Zdiv_mult_le:
-- 
cgit v1.2.3