Factor related_Z_op (except conditional_sub)

1 files changed, 13 insertions, 0 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
new file mode 100644
index 000000000..bb833507f
--- /dev/null
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
@@ -0,0 +1,13 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+
+Lemma neg_nonneg : forall x y, 0 <= ModularBaseSystemListZOperations.neg x y.
+Proof. Admitted.
+Hint Resolve neg_nonneg : zarith.
+Lemma neg_upperbound : forall x y, ModularBaseSystemListZOperations.neg x y <= Z.ones x.
+Proof. Admitted.
+Hint Resolve neg_upperbound : zarith.