Add ext_limb_widths_upper_bound

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m00.15s | Total                                           | 1m00.12s || +0m00.03s
----------------------------------------------------------------------------------
0m14.85s | Specific/GF25519                                | 0m16.44s || -0m01.59s
0m16.98s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.66s || +0m00.32s
0m04.21s | ModularArithmetic/Pow2BaseProofs                | 0m04.23s || -0m00.02s
0m03.81s | BaseSystemProofs                                | 0m03.96s || -0m00.14s
0m03.33s | Experiments/SpecificCurve25519                  | 0m03.33s || +0m00.00s
0m03.01s | Util/ListUtil                                   | 0m02.98s || +0m00.02s
0m02.43s | Specific/GF1305                                 | 0m02.00s || +0m00.43s
0m02.11s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.05s || +0m00.06s
0m01.45s | BaseSystem                                      | 0m01.16s || +0m00.29s
0m01.21s | ModularArithmetic/ExtendedBaseVector            | 0m01.17s || +0m00.04s
0m00.91s | ModularArithmetic/ModularBaseSystemField        | 0m00.90s || +0m00.01s
0m00.83s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.76s || +0m00.06s
0m00.70s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.58s || +0m00.12s
0m00.66s | Testbit                                         | 0m00.63s || +0m00.03s
0m00.64s | ModularArithmetic/ModularBaseSystemList         | 0m00.58s || +0m00.06s
0m00.62s | Util/AdditionChainExponentiation                | 0m00.62s || +0m00.00s
0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.55s || +0m00.05s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.60s || +0m00.00s
0m00.60s | ModularArithmetic/ModularBaseSystem             | 0m00.55s || +0m00.04s
0m00.60s | ModularArithmetic/Pow2Base                      | 0m00.38s || +0m00.21s

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 6c1da1311..0c1ff5ccd 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1072,6 +1072,16 @@ Qed.
 
 Hint Rewrite @sum_firstn_all_succ using omega : simpl_sum_firstn.
 
+Lemma sum_firstn_all : forall n l, (length l <= n)%nat ->
+  sum_firstn l n = sum_firstn l (length l).
+Proof.
+  unfold sum_firstn; intros.
+  rewrite !firstn_all_strong by omega.
+  congruence.
+Qed.
+
+Hint Rewrite @sum_firstn_all using omega : simpl_sum_firstn.
+
 Lemma sum_firstn_succ_default : forall l i,
   sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z.
 Proof.
@@ -1139,6 +1149,40 @@ Qed.
 
 Hint Resolve sum_firstn_nonnegative : znonzero.
 
+Lemma sum_firstn_app : forall xs ys n,
+  sum_firstn (xs ++ ys) n = (sum_firstn xs n + sum_firstn ys (n - length xs))%Z.
+Proof.
+  induction xs; simpl.
+  { intros ys n; autorewrite with simpl_sum_firstn; simpl.
+    f_equal; omega. }
+  { intros ys [|n]; autorewrite with simpl_sum_firstn; simpl; [ reflexivity | ].
+    rewrite IHxs; omega. }
+Qed.
+
+Lemma sum_firstn_app_sum : forall xs ys n,
+  sum_firstn (xs ++ ys) (length xs + n) = (sum_firstn xs (length xs) + sum_firstn ys n)%Z.
+Proof.
+  intros; rewrite sum_firstn_app; autorewrite with simpl_sum_firstn.
+  do 2 f_equal; omega.
+Qed.
+
+Hint Rewrite @sum_firstn_app_sum : simpl_sum_firstn.
+
+Definition NotSum {T} (xs : list T) (v : nat) := True.
+
+Ltac NotSum :=
+  lazymatch goal with
+  | [ |- NotSum ?xs (length ?xs + _)%nat ] => fail
+  | [ |- NotSum _ _ ] => exact I
+  end.
+
+Lemma sum_firstn_app_hint : forall xs ys n, NotSum xs n ->
+  sum_firstn (xs ++ ys) n = (sum_firstn xs n + sum_firstn ys (n - length xs))%Z.
+Proof. auto using sum_firstn_app. Qed.
+
+Hint Rewrite sum_firstn_app_hint using solve [ NotSum ] : simpl_sum_firstn.
+
+
 Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
   nth_default d (map2 f ls1 ls2) i =
     if lt_dec i (min (length ls1) (length ls2))