val lemma_prime: unit -> Lemma (pow2 130 % prime = 5)
let lemma_prime () =
  assert_norm (pow2 130 % prime = 5 % prime);
  assert_norm (5 < prime);
  FStar.Math.Lemmas.modulo_lemma 5 prime
val lemma_prime: unit -> Lemma (pow2 130 % prime = 5)
let lemma_prime () =
assert_norm (pow2 130 % prime = 5 % prime);
assert_norm (5 < prime);
FStar.Math.Lemmas.modulo_lemma 5 prime
Hacl.Poly1305.Field32xN.Lemmas0.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Poly1305.Field32xN.Lemmas0.fst
Prims.unit FStar.Math.Lemmas.modulo_lemma Hacl.Spec.Poly1305.Vec.prime FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Prims.op_Modulus Prims.pow2
module Hacl.Poly1305.Field32xN.Lemmas0

open Lib.IntTypes
open Lib.IntVector
open Lib.Sequence
open FStar.Mul
open FStar.Calc

open Hacl.Spec.Poly1305.Vec
include Hacl.Spec.Poly1305.Field32xN

#reset-options "--z3rlimit 50 --using_facts_from '* -FStar.Seq' --max_fuel 0 --max_ifuel 0"

val lemma_prime: unit -> Lemma (pow2 130 % prime = 5)
val lemma_prime: unit -> Lemma (pow2 130 % prime = 5)
_: Prims.unit -> FStar.Pervasives.Lemma (ensures Prims.pow2 130 % Hacl.Spec.Poly1305.Vec.prime = 5)