Specific/GF25519: Updated to match new PseudoMersenneBaseParams spec.

1 files changed, 10 insertions, 2 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 650990252..68d259881 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -74,11 +74,19 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
   Lemma base_succ : forall i, ((S i) < length base)%nat -> 
     let b := nth_default 0 base in
     b (S i) mod b i = 0.
-  Admitted.
+  Proof.
+    intros.
+    assert (In i (seq 0 (length base))) by nth_tac.
+    assert (In (S i) (seq 0 (length base))) by nth_tac.
+    subst b; simpl in *.
+    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+  Qed.
 
   Lemma base_tail_matches_modulus:
     2^k mod nth_default 0 base (pred (length base)) = 0.
-  Admitted.
+  Proof.
+    nth_tac.
+  Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
   Proof.