diff options
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. |