val one_mod : SE.one_st S.qelem mk_to_nat_mod_comm_monoid
let one_mod _ = 1
val one_mod : SE.one_st S.qelem mk_to_nat_mod_comm_monoid
let one_mod _ =
1
Hacl.Spec.K256.Qinv.fst.checked
Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.NatMod.fsti.checked Lib.Exponentiation.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.Qinv.fst
Prims.unit Spec.K256.PointOps.qelem
module Hacl.Spec.K256.Qinv

open FStar.Mul

module SE = Spec.Exponentiation
module LE = Lib.Exponentiation
module M = Lib.NatMod
module S = Spec.K256

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

let nat_mod_comm_monoid = M.mk_nat_mod_comm_monoid S.q

let mk_to_nat_mod_comm_monoid : SE.to_comm_monoid S.qelem = {
  SE.a_spec = S.qelem;
  SE.comm_monoid = nat_mod_comm_monoid;
  SE.refl = (fun (x:S.qelem) -> x);
}
val one_mod : SE.one_st S.qelem mk_to_nat_mod_comm_monoid
Spec.Exponentiation.one_st Spec.K256.PointOps.qelem Hacl.Spec.K256.Qinv.mk_to_nat_mod_comm_monoid