diff options
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v | 13 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 2 |
2 files changed, 11 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v index bb833507f..5d9e64901 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v @@ -5,9 +5,14 @@ Require Import Crypto.Util.ZUtil. Local Open Scope Z_scope. -Lemma neg_nonneg : forall x y, 0 <= ModularBaseSystemListZOperations.neg x y. -Proof. Admitted. +Lemma neg_nonneg : forall x y, 0 <= x -> 0 <= ModularBaseSystemListZOperations.neg x y. +Proof. + unfold neg; intros; break_match; auto with zarith. +Qed. Hint Resolve neg_nonneg : zarith. -Lemma neg_upperbound : forall x y, ModularBaseSystemListZOperations.neg x y <= Z.ones x. -Proof. Admitted. + +Lemma neg_upperbound : forall x y, 0 <= x -> ModularBaseSystemListZOperations.neg x y <= Z.ones x. +Proof. + unfold neg; intros; break_match; auto with zarith. +Qed. Hint Resolve neg_upperbound : zarith. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 17e8d62bf..9dc4eeb51 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -944,6 +944,7 @@ Module Z. rewrite Z.ones_succ by assumption. zero_bounds. Qed. + Hint Resolve ones_nonneg : zarith. Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. Proof. @@ -953,6 +954,7 @@ Module Z. apply Z.lt_succ_lt_pred. apply Z.pow_gt_1; omega. Qed. + Hint Resolve ones_pos_pos : zarith. Lemma pow2_mod_id_iff : forall a n, 0 <= n -> (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). |