From 8c1735389e54d6ed4d8552a9e3f568d5edc5fa72 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 25 Mar 2019 11:02:25 +0100 Subject: 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.) --- lib/Integers.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'lib/Integers.v') 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 *) -- cgit