diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:02:25 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:02:25 +0100 |
| commit | 8c1735389e54d6ed4d8552a9e3f568d5edc5fa72 (patch) | |
| tree | 382e2e48bab10bc44e1d3c7a03ca4aff28f09073 | |
| parent | 02015cafba394b4e18c6231204c5838724b31297 (diff) | |
| download | compcert-8c1735389e54d6ed4d8552a9e3f568d5edc5fa72.tar.gz compcert-8c1735389e54d6ed4d8552a9e3f568d5edc5fa72.zip | |
Integers.v: add modulus_gt_one (#259)
Since the number of bits is > 0, it is guaranteed that
modulus > 1, not just that modulus > 0.
(Suggested by Jake Waksbaum @jbaum.)
| -rw-r--r-- | lib/Integers.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 0e506208..4b75e71e 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -80,9 +80,15 @@ Proof. unfold modulus. apply two_power_nat_two_p. Qed. +Remark modulus_gt_one: modulus > 1. +Proof. + rewrite modulus_power. apply Z.lt_gt. apply (two_p_monotone_strict 0). + generalize wordsize_pos; omega. +Qed. + Remark modulus_pos: modulus > 0. Proof. - rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega. + generalize modulus_gt_one; omega. Qed. (** * Representation of machine integers *) |