diff options
Diffstat (limited to 'theories/ZArith/Zquot.v')
| -rw-r--r-- | theories/ZArith/Zquot.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 3ef111898..6db92edb7 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -243,7 +243,7 @@ Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. -(** Some additionnal inequalities about Zdiv. *) +(** Some additional inequalities about Zdiv. *) Theorem Zquot_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a÷b <= q. |