val prime:pos
let prime: pos = Scalar.prime
val prime:pos
let prime:pos =
Scalar.prime
Hacl.Spec.Poly1305.Lemmas.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.fst.checked
Hacl.Spec.Poly1305.Lemmas.fst
Spec.Poly1305.prime
module Hacl.Spec.Poly1305.Lemmas

open FStar.Mul
module Scalar = Spec.Poly1305

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

/// Semiring for Poly1305

#set-options "--z3rlimit 5 --max_fuel 0 --max_ifuel 0 --z3cliopt smt.arith.nl=false"
val prime:pos
Prims.pos