val lemma_feval_is_fas_nat:
    #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)} ->
  Lemma (forall (i:nat). i < w ==> (fas_nat5 f).[i] == (feval5 f).[i])
let lemma_feval_is_fas_nat #w f =
  FStar.Classical.forall_intro (lemma_feval_is_fas_nat_i #w f)
val lemma_feval_is_fas_nat:
    #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)} ->
  Lemma (forall (i:nat). i < w ==> (fas_nat5 f).[i] == (feval5 f).[i])
let lemma_feval_is_fas_nat #w f =
FStar.Classical.forall_intro (lemma_feval_is_fas_nat_i #w f)
Hacl.Spec.Poly1305.Field32xN.Lemmas.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 Hacl.Poly1305.Field32xN.Lemmas2.fst.checked Hacl.Poly1305.Field32xN.Lemmas1.fst.checked Hacl.Poly1305.Field32xN.Lemmas0.fst.checked Hacl.Impl.Poly1305.Lemmas.fst.checked FStar.UInt32.fsti.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.Spec.Poly1305.Field32xN.Lemmas.fst
Hacl.Spec.Poly1305.Field32xN.lanes Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Spec.Poly1305.Field32xN.felem_less5 Prims.pow2 FStar.Classical.forall_intro Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.nat Prims.l_or Prims.l_and Spec.Poly1305.prime Hacl.Spec.Poly1305.Vec.pfelem FStar.Seq.Base.index Lib.Sequence.to_seq Hacl.Spec.Poly1305.Field32xN.feval5 Hacl.Spec.Poly1305.Field32xN.fas_nat5 Lib.Sequence.op_String_Access Hacl.Spec.Poly1305.Field32xN.Lemmas.lemma_feval_is_fas_nat_i Prims.unit
module Hacl.Spec.Poly1305.Field32xN.Lemmas

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

open Hacl.Spec.Poly1305.Field32xN
open Hacl.Poly1305.Field32xN.Lemmas0
open Hacl.Poly1305.Field32xN.Lemmas1
open Hacl.Poly1305.Field32xN.Lemmas2

module Vec = Hacl.Spec.Poly1305.Vec

#set-options "--z3rlimit 100 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --using_facts_from '* -FStar.Seq'"


val lemma_feval_is_fas_nat_i:
  #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)}
  -> i:size_nat{i < w} ->
  Lemma ((feval5 f).[i] == (fas_nat5 f).[i])

let lemma_feval_is_fas_nat_i #w f i =
  assert_norm (pow2 128 < Vec.prime);
  assert ((feval5 f).[i] == (as_nat5 (transpose f).[i]) % Vec.prime);
  FStar.Math.Lemmas.modulo_lemma (as_nat5 (transpose f).[i]) Vec.prime

val lemma_feval_is_fas_nat:
    #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)} ->
  Lemma (forall (i:nat). i < w ==> (fas_nat5 f).[i] == (feval5 f).[i])
val lemma_feval_is_fas_nat:
    #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)} ->
  Lemma (forall (i:nat). i < w ==> (fas_nat5 f).[i] == (feval5 f).[i])

    f:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        {Hacl.Spec.Poly1305.Field32xN.felem_less5 f (Prims.pow2 128)}
  -> FStar.Pervasives.Lemma
    (ensures
      forall (i: Prims.nat).
        i < w ==>
        (Hacl.Spec.Poly1305.Field32xN.fas_nat5 f).[ i ] ==
        (Hacl.Spec.Poly1305.Field32xN.feval5 f).[ i ])