diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-08 13:10:35 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-08 13:10:35 -0500 |
| commit | b103fcc6f1d130cc4c6d9200851f62a392c1d798 (patch) | |
| tree | af025f9d535ab908e10abae60e789444f23a2f78 /src/ModularArithmetic | |
| parent | c89a77f3b6de068aaf1b8cd2adad73ef64c7fb13 (diff) | |
Prove things in ModularBaseSystemListZOperationsProofs
Diffstat (limited to 'src/ModularArithmetic')
| -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. |