From b103fcc6f1d130cc4c6d9200851f62a392c1d798 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 8 Nov 2016 13:10:35 -0500 Subject: Prove things in ModularBaseSystemListZOperationsProofs --- .../ModularBaseSystemListZOperationsProofs.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3