Move more proofs earlier

2 files changed, 16 insertions, 12 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index d4df6040f..ddf787d21 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -160,3 +160,5 @@ Section ExtendedBaseVector.
     unfold ext_base; rewrite app_length; rewrite map_length; auto.
   Qed.
 End ExtendedBaseVector.
+
+Hint Rewrite @extended_base_length : distr_length.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index daff60220..227a3e77f 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -128,27 +128,29 @@ Section PseudoMersenneProofs.
     subst; auto.
   Qed.
 
-  Lemma decode_short : forall (us : BaseSystem.digits),
-    (length us <= length base)%nat ->
-    BaseSystem.decode base us = BaseSystem.decode ext_base us.
+  Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits),
+      (length us <= length base)%nat
+      -> firstn (length us) base = firstn (length us) ext_base.
   Proof.
-    intros.
-    unfold BaseSystem.decode, BaseSystem.decode'.
-    rewrite combine_truncate_r.
-    rewrite (combine_truncate_r us ext_base).
-    f_equal; f_equal.
-    unfold ext_base.
+    unfold ext_base; intros.
     rewrite firstn_app_inleft; auto; omega.
   Qed.
+  Local Hint Immediate firstn_us_base_ext_base.
+
+  Lemma decode_short : forall (us : BaseSystem.digits),
+    (length us <= length base)%nat ->
+    BaseSystem.decode base us = BaseSystem.decode ext_base us.
+  Proof. auto using decode_short_initial. Qed.
+
+  Local Hint Immediate ExtBaseVector.
 
   Lemma mul_rep_extended : forall (us vs : BaseSystem.digits),
       (length us <= length base)%nat ->
       (length vs <= length base)%nat ->
       (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs).
   Proof.
-      intros.
-      rewrite mul_rep by (apply ExtBaseVector || unfold ext_base; simpl_list; omega).
-      f_equal; rewrite decode_short; auto.
+    intros; apply mul_rep_two_base; auto;
+      autorewrite with distr_length; try omega.
   Qed.
 
   Lemma modulus_nonzero : modulus <> 0.