aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v8
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivFloor.v8
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivTrunc.v8
3 files changed, 24 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ce49877e4..967b68d36 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 ca6197002..a9077127e 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 46c36015d..bbb8ad5ae 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: