diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index f19baf4d16..0e54c453b7 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -88,7 +88,7 @@ Theorem div_unique_pos: Proof. intros; apply div_unique with r; auto. Qed. Theorem div_unique_neg: - forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b. + forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b. Proof. intros; apply div_unique with r; auto. Qed. Theorem mod_unique: |