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/Natural | |
| 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/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 47f409605..105051611 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -47,6 +47,9 @@ Theorem mod_unique: forall a b q r, r<b -> a == b*q + r -> r == a mod b. Proof. intros. apply mod_unique with q; auto'. Qed. +Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b. +Proof. intros. apply div_unique_exact; auto'. Qed. + (** A division by itself returns 1 *) Lemma div_same : forall a, a~=0 -> a/a == 1. @@ -236,4 +239,3 @@ Lemma mod_divides : forall a b, b~=0 -> Proof. intros. apply mod_divides; auto'. Qed. End NDivProp. - |