Weaker UniformBase assumptions

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
0m59.51s | Total                                           | 0m59.14s || +0m00.37s
----------------------------------------------------------------------------------
0m16.46s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.45s || +0m00.01s
0m14.41s | Specific/GF25519                                | 0m14.36s || +0m00.05s
0m08.35s | ModularArithmetic/Pow2BaseProofs                | 0m08.58s || -0m00.23s
0m04.71s | Testbit                                         | 0m04.33s || +0m00.37s
0m03.41s | Experiments/SpecificCurve25519                  | 0m03.31s || +0m00.10s
0m02.09s | Specific/GF1305                                 | 0m02.05s || +0m00.04s
0m02.02s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.09s || -0m00.06s
0m01.71s | ModularArithmetic/BarrettReduction/ZBounded     | 0m01.70s || +0m00.01s
0m01.15s | ModularArithmetic/ExtendedBaseVector            | 0m01.16s || -0m00.01s
0m00.91s | ModularArithmetic/Montgomery/ZBounded           | 0m00.84s || +0m00.07s
0m00.90s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.92s || -0m00.02s
0m00.86s | ModularArithmetic/ModularBaseSystemField        | 0m00.90s || -0m00.04s
0m00.69s | ModularArithmetic/ModularBaseSystemList         | 0m00.61s || +0m00.07s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.66s || -0m00.01s
0m00.61s | ModularArithmetic/ModularBaseSystem             | 0m00.57s || +0m00.04s
0m00.59s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.62s || -0m00.03s

2 files changed, 5 insertions, 4 deletions

diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 8f115f101..9a31bef59 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -692,8 +692,8 @@ Section BitwiseDecodeEncode.
 End BitwiseDecodeEncode.
 
 Section UniformBase.
-  Context {width : Z} (limb_width_pos : 0 < width).
-  Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil)
+  Context {width : Z} (limb_width_nonneg : 0 <= width).
+  Context (limb_widths : list Z)
     (limb_widths_uniform : forall w, In w limb_widths -> w = width).
   Local Notation base := (base_from_limb_widths limb_widths).
 
@@ -721,7 +721,6 @@ Section UniformBase.
   Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
   Proof.
     intros.
-    apply Z.lt_le_incl.
     replace w with width by (symmetry; auto).
     assumption.
   Qed.
diff --git a/src/Testbit.v b/src/Testbit.v
index 6bc693fae..c7e698e04 100644
--- a/src/Testbit.v
+++ b/src/Testbit.v
@@ -33,7 +33,7 @@ Section Testbit.
            | H : ~ (_ = _ :> nat) |- _ => unique pose proof (fun x => H (Nat2Z.inj _ _ x))
            | H : (_ = _ :> nat) |- _ => unique pose proof (proj2 (Nat2Z.inj_iff _ _) H)
            end.
-  
+
   Lemma testbit_spec' : forall a b us, (0 <= b < width) ->
     bounded limb_widths us -> (length us = length limb_widths)%nat ->
     Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b).
@@ -42,6 +42,8 @@ Section Testbit.
              | |- _ => progress intros
              | |- _ => progress autorewrite with push_nth_default Ztestbit zsimplify in *
              | |- _ => progress change (Z.of_nat 0) with 0 in *
+             | [ H : In ?x ?ls, H' : forall x', In x' ?ls -> x' = _ |- _ ]
+               => is_var x; apply H' in H
              | |- _ => rewrite Nat2Z.inj_succ, Z.mul_succ_l
              | |- _ => rewrite nth_default_out_of_bounds by omega
              | |- _ => rewrite nth_default_uniform_base by omega