added proofs about addition chain exponentiation for later use in ModularBaseSystem [pow], which we need for sqrt and inversion.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 0afc07c5d..65d899463 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -10,7 +10,7 @@ Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Notations.
 
 Module E.
-  Import Group Ring Field CompleteEdwardsCurve.E.
+  Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
   Section CompleteEdwardsCurveTheorems.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}