diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v | 13 |
1 files changed, 9 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. |