From ac116a5b734aba589b923ba00bae56d244360af8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Nov 2016 15:50:12 -0500 Subject: Update bounds things with prefreeze --- src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v index 5d9e64901..6163650e4 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v @@ -16,3 +16,13 @@ Proof. unfold neg; intros; break_match; auto with zarith. Qed. Hint Resolve neg_upperbound : zarith. + +Lemma neg_range : forall x y, 0 <= x -> + 0 <= neg x y < 2 ^ x. +Proof. + intros. + split; auto using neg_nonneg. + eapply Z.le_lt_trans; eauto using neg_upperbound. + rewrite Z.ones_equiv. + omega. +Qed. -- cgit v1.2.3