diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:12 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:12 +0000 |
commit | 7e00447c512b71543cec6b6fd63ec44106dada3d (patch) | |
tree | be7c091aa47ec424f7108efbe96d2713fc69ccab /theories/Numbers/Integer/Abstract | |
parent | 81c4c8bc418cdf42cc88249952dbba465068202c (diff) |
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
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 5 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 5 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 5 |
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. |