val elem_add_cm:cm elem
let elem_add_cm : cm elem =
  CM zero ( +% ) (LM.lemma_add_mod_one #prime) (LM.lemma_add_mod_assoc #prime) (LM.lemma_add_mod_comm #prime)
val elem_add_cm:cm elem
let elem_add_cm:cm elem =
CM zero
  ( +% )
  (LM.lemma_add_mod_one #prime)
  (LM.lemma_add_mod_assoc #prime)
  (LM.lemma_add_mod_comm #prime)
Spec.Ed25519.Lemmas.fst.checked
Spec.Ed25519.PointOps.fst.checked Spec.Curve25519.Lemmas.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.NatMod.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Fermat.fsti.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.fst.checked
Spec.Ed25519.Lemmas.fst
FStar.Algebra.CommMonoid.CM Spec.Curve25519.elem Spec.Curve25519.zero Spec.Curve25519.op_Plus_Percent Lib.NatMod.lemma_add_mod_one Spec.Curve25519.prime Lib.NatMod.lemma_add_mod_assoc Lib.NatMod.lemma_add_mod_comm
module Spec.Ed25519.Lemmas

open FStar.Mul

module Fermat = FStar.Math.Fermat
module Euclid = FStar.Math.Euclid

module LE = Lib.Exponentiation
module LM = Lib.NatMod

open Spec.Curve25519
open Spec.Curve25519.Lemmas
open Spec.Ed25519.PointOps

open FStar.Algebra.CommMonoid
open FStar.Tactics.CanonCommSemiring
open FStar.Tactics

#set-options "--z3rlimit 50 --ifuel 0 --fuel 0"

[@canon_attr]
noextract
val elem_add_cm:cm elem
FStar.Algebra.CommMonoid.cm Spec.Curve25519.elem