val lemma_pow2_128: n:nat ->
  Lemma
  (requires n <= 128)
  (ensures pow2 n < Scalar.prime)
  [SMTPat (pow2 n)]
let lemma_pow2_128 n =
  Math.Lemmas.pow2_le_compat 128 n;
  assert (pow2 n <= pow2 128);
  assert_norm (pow2 128 < Scalar.prime)
val lemma_pow2_128: n:nat ->
  Lemma
  (requires n <= 128)
  (ensures pow2 n < Scalar.prime)
  [SMTPat (pow2 n)]
let lemma_pow2_128 n =
Math.Lemmas.pow2_le_compat 128 n;
assert (pow2 n <= pow2 128);
assert_norm (pow2 128 < Scalar.prime)
Hacl.Spec.Poly1305.Vec.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Poly1305.Vec.fst
Prims.nat FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Spec.Poly1305.prime Prims.unit Prims._assert Prims.op_LessThanOrEqual FStar.Math.Lemmas.pow2_le_compat
module Hacl.Spec.Poly1305.Vec

#reset-options "--z3rlimit 60 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"

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

module Scalar = Spec.Poly1305

(* Field types and parameters *)
val lemma_pow2_128: n:nat ->
  Lemma
  (requires n <= 128)
  (ensures pow2 n < Scalar.prime)
  [SMTPat (pow2 n)]
val lemma_pow2_128: n:nat ->
  Lemma
  (requires n <= 128)
  (ensures pow2 n < Scalar.prime)
  [SMTPat (pow2 n)]
n: Prims.nat
  -> FStar.Pervasives.Lemma (requires n <= 128)
      (ensures Prims.pow2 n < Spec.Poly1305.prime)
      [SMTPat (Prims.pow2 n)]