Prove things in ModularBaseSystemListZOperationsProofs

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).