val elem_cr:cr elem
let elem_cr : cr elem =
  CR elem_add_cm elem_mul_cm ( ~% ) fadd_opp (LM.lemma_mod_distributivity_add_right #prime) fmul_zero_l
val elem_cr:cr elem
let elem_cr:cr elem =
CR elem_add_cm
  elem_mul_cm
  ( ~% )
  fadd_opp
  (LM.lemma_mod_distributivity_add_right #prime)
  fmul_zero_l
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.Tactics.CanonCommSemiring.CR Spec.Curve25519.elem Spec.Ed25519.Lemmas.elem_add_cm Spec.Ed25519.Lemmas.elem_mul_cm Spec.Ed25519.Lemmas.op_Tilde_Percent Spec.Ed25519.Lemmas.fadd_opp Lib.NatMod.lemma_mod_distributivity_add_right Spec.Curve25519.prime Spec.Ed25519.Lemmas.fmul_zero_l
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)
let fadd_opp a =
  FStar.Math.Lemmas.lemma_mod_add_distr a (-a) prime;
  FStar.Math.Lemmas.small_mod 0 prime

[@canon_attr]
noextract
val elem_cr:cr elem
FStar.Tactics.CanonCommSemiring.cr Spec.Curve25519.elem