aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ExtendedBaseVector.v
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-07-25 21:06:07 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-07-25 21:06:07 -0400
commit39a6c95de8a900c859726d875cc40ea96298d31b (patch)
tree750571dc101f477c34340716db87a3697cca41eb /src/ModularArithmetic/ExtendedBaseVector.v
parentea9397e3da37f35d088488be141cb18cc38ea11b (diff)
Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
Diffstat (limited to 'src/ModularArithmetic/ExtendedBaseVector.v')
-rw-r--r--src/ModularArithmetic/ExtendedBaseVector.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index fcd871aae..ef8c9716a 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -122,6 +122,7 @@ Section ExtendedBaseVector.
rewrite (map_nth_default _ _ _ _ 0) by omega.
apply base_matches_modulus; auto using limb_widths_nonnegative, limb_widths_match_modulus;
distr_length.
+ assumption.
} { (* i < length base, j >= length base, i + j >= length base *)
do 2 rewrite map_nth_default_base_high by omega.
remember (j - length base)%nat as j'.