let nat_mod_comm_monoid = M.mk_nat_mod_comm_monoid S.prime
let nat_mod_comm_monoid =
M.mk_nat_mod_comm_monoid S.prime
Hacl.Spec.P256.Finv.fst.checked
Spec.P256.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.P256.Finv.fst
Lib.NatMod.mk_nat_mod_comm_monoid Spec.P256.PointOps.prime
module Hacl.Spec.P256.Finv

open FStar.Mul

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

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val nat_mod_comm_monoid : Lib.Exponentiation.Definition.comm_monoid (Lib.NatMod.nat_mod Spec.P256.PointOps.prime)
Lib.Exponentiation.Definition.comm_monoid (Lib.NatMod.nat_mod Spec.P256.PointOps.prime)