val bn_v_is_as_nat: e:lseq uint64 4 ->
  Lemma (as_nat4 (e.[0], e.[1], e.[2], e.[3]) == Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e)
let bn_v_is_as_nat e =
  Hacl.Impl.Curve25519.Lemmas.lemma_nat_from_uints64_le_4 e;
  assert (as_nat4 (e.[0], e.[1], e.[2], e.[3]) == Lib.ByteSequence.nat_from_intseq_le e);
  Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma 4 e;
  assert (Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e == Lib.ByteSequence.nat_from_intseq_le e)
val bn_v_is_as_nat: e:lseq uint64 4 ->
  Lemma (as_nat4 (e.[0], e.[1], e.[2], e.[3]) == Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e)
let bn_v_is_as_nat e =
Hacl.Impl.Curve25519.Lemmas.lemma_nat_from_uints64_le_4 e;
assert (as_nat4 (e.[ 0 ], e.[ 1 ], e.[ 2 ], e.[ 3 ]) == Lib.ByteSequence.nat_from_intseq_le e);
Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma 4 e;
assert (Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e == Lib.ByteSequence.nat_from_intseq_le e)
Hacl.Spec.Curve25519.Field64.Definition.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Curve25519.Field64.Definition.fst
Lib.Sequence.lseq Lib.IntTypes.uint64 Prims._assert Prims.eq2 Prims.nat Hacl.Spec.Bignum.Definitions.bn_v Lib.IntTypes.U64 Lib.ByteSequence.nat_from_intseq_le Lib.IntTypes.SEC Prims.unit Hacl.Spec.Bignum.Convert.bn_v_is_nat_from_intseq_le_lemma Hacl.Spec.Curve25519.Field64.Definition.as_nat4 FStar.Pervasives.Native.Mktuple4 Lib.Sequence.op_String_Access Hacl.Impl.Curve25519.Lemmas.lemma_nat_from_uints64_le_4
module Hacl.Spec.Curve25519.Field64.Definition

open Lib.Sequence
open Lib.IntTypes

module P = Spec.Curve25519

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let felem4 = (uint64 * uint64 * uint64 * uint64)

open FStar.Mul

noextract
val as_nat4: f:felem4 -> GTot nat
let as_nat4 f =
  let (s0, s1, s2, s3) = f in
  v s0 + v s1 * pow2 64 + v s2 * pow2 64 * pow2 64 +
  v s3 * pow2 64 * pow2 64 * pow2 64

let feval4 (f:felem4) : GTot P.elem = as_nat4 f % P.prime


val bn_v_is_as_nat: e:lseq uint64 4 ->
  Lemma (as_nat4 (e.[0], e.[1], e.[2], e.[3]) == Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e)
val bn_v_is_as_nat: e:lseq uint64 4 ->
  Lemma (as_nat4 (e.[0], e.[1], e.[2], e.[3]) == Hacl.Spec.Bignum.Definitions.bn_v #U64 #4 e)
e: Lib.Sequence.lseq Lib.IntTypes.uint64 4
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Curve25519.Field64.Definition.as_nat4 (e.[ 0 ], e.[ 1 ], e.[ 2 ], e.[ 3 ]) ==
      Hacl.Spec.Bignum.Definitions.bn_v e)