1 files changed, 13 insertions, 0 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
new file mode 100644
index 000000000..8bc3d6e20
--- /dev/null
+++ b/src/Curves/Curve25519.v
@@ -0,0 +1,13 @@
+
+Require Import ZModulo.
+(**
+ * The relevant module is ZModulo:
+ *   the constructor you want is of_pos
+ *   the operations you want are in zmod_ops
+ *   the tactics you want are somewhere between Field and CyclicType:
+ *     probs you want to be converting to/from Z pretty frequently
+ *
+ * Coq Reference page:
+ *    https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html
+ *)
+