Numbers: a particular case of div_unique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 15 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index e1802dbee..954b89150 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 bc1932d44..f19baf4d1 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 09f9e023e..74abedb42 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.