val fadd_opp (a:elem) : Lemma (a +% ~%a == zero)
let fadd_opp a =
  FStar.Math.Lemmas.lemma_mod_add_distr a (-a) prime;
  FStar.Math.Lemmas.small_mod 0 prime
val fadd_opp (a:elem) : Lemma (a +% ~%a == zero)
let fadd_opp a =
FStar.Math.Lemmas.lemma_mod_add_distr a (- a) prime;
FStar.Math.Lemmas.small_mod 0 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
Spec.Curve25519.elem FStar.Math.Lemmas.small_mod Spec.Curve25519.prime Prims.unit FStar.Math.Lemmas.lemma_mod_add_distr Prims.op_Minus
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
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)

[@canon_attr]
noextract
let elem_mul_cm : cm elem =
  CM one ( *% ) (LM.lemma_mul_mod_one #prime) (LM.lemma_mul_mod_assoc #prime) (LM.lemma_mul_mod_comm #prime)

val fmul_zero_l: mult_zero_l_lemma elem elem_add_cm elem_mul_cm
let fmul_zero_l a = assert_norm (forall x. zero *% x == zero)

let ( ~% ) (a:elem) : elem = (-a) % prime

val fadd_opp (a:elem) : Lemma (a +% ~%a == zero)
val fadd_opp (a:elem) : Lemma (a +% ~%a == zero)
a: Spec.Curve25519.elem -> FStar.Pervasives.Lemma (ensures a +% ~%a == Spec.Curve25519.zero)