diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 15:50:12 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 15:50:12 -0500 |
| commit | ac116a5b734aba589b923ba00bae56d244360af8 (patch) | |
| tree | 47b8c550da866a37b0d674b228c8d56e900e01ce /src/ModularArithmetic | |
| parent | 9f9fa521e29293af46123b1c97fd1426d0cf240a (diff) | |
Update bounds things with prefreeze
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |