diff options
Diffstat (limited to 'lib/Integers.v')
| -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 *) |