3 files changed, 15 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index e1802dbeeb..954b89150a 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -268,6 +268,11 @@ Proof.
 intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
 Qed.
 
+Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul.
+Qed.
+
 (** * Order results about mod and div *)
 
 (** A modulo cannot grow beyond its starting point. *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index bc1932d446..f19baf4d16 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -316,6 +316,11 @@ Proof.
 intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
 Qed.
 
+Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul.
+Qed.
+
 (** * Order results about mod and div *)
 
 (** A modulo cannot grow beyond its starting point. *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 09f9e023eb..74abedb423 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -178,6 +178,11 @@ Proof.
 intros. rewrite rem_eq, quot_mul by trivial. rewrite mul_comm; apply sub_diag.
 Qed.
 
+Theorem quot_unique_exact a b q: b~=0 -> a == b*q -> q == a÷b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply quot_mul.
+Qed.
+
 (** The sign of [a rem b] is the one of [a] (when it's not null) *)
 
 Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b.