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 ++++++++
 3 files changed, 24 insertions(+)

(limited to 'theories/Numbers')

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:
-- 
cgit v1.2.3