val lemma_nat_from_uints64_le_4: b:lseq uint64 4 -> Lemma
  (nat_from_intseq_le b == v b.[0] + v b.[1] * pow2 64 +
    v b.[2] * pow2 64 * pow2 64 + v b.[3] * pow2 64 * pow2 64 * pow2 64)
let lemma_nat_from_uints64_le_4 b =
  let res = nat_from_intseq_le b in
  nat_from_intseq_le_slice_lemma b 1;
  nat_from_intseq_le_lemma0 (Seq.slice b 0 1);
  assert (res == v b.[0] + pow2 64 * (nat_from_intseq_le (Seq.slice b 1 4)));

  nat_from_intseq_le_slice_lemma #U64 #SEC #3 (Seq.slice b 1 4) 1;
  nat_from_intseq_le_lemma0 (Seq.slice b 1 2);
  assert (nat_from_intseq_le (Seq.slice b 1 4) == v b.[1] + pow2 64 * (nat_from_intseq_le (Seq.slice b 2 4)));

  nat_from_intseq_le_slice_lemma #U64 #SEC #2 (Seq.slice b 2 4) 1;
  nat_from_intseq_le_lemma0 (Seq.slice b 2 3);
  assert (nat_from_intseq_le (Seq.slice b 2 4) == v b.[2] + pow2 64 * (nat_from_intseq_le (Seq.slice b 3 4)));

  nat_from_intseq_le_lemma0 (Seq.slice b 3 4);
  assert (res == v b.[0] + pow2 64 * (v b.[1] + pow2 64 * (v b.[2] + pow2 64 * v b.[3])))
val lemma_nat_from_uints64_le_4: b:lseq uint64 4 -> Lemma
  (nat_from_intseq_le b == v b.[0] + v b.[1] * pow2 64 +
    v b.[2] * pow2 64 * pow2 64 + v b.[3] * pow2 64 * pow2 64 * pow2 64)
let lemma_nat_from_uints64_le_4 b =
let res = nat_from_intseq_le b in
nat_from_intseq_le_slice_lemma b 1;
nat_from_intseq_le_lemma0 (Seq.slice b 0 1);
assert (res == v b.[ 0 ] + pow2 64 * (nat_from_intseq_le (Seq.slice b 1 4)));
nat_from_intseq_le_slice_lemma #U64 #SEC #3 (Seq.slice b 1 4) 1;
nat_from_intseq_le_lemma0 (Seq.slice b 1 2);
assert (nat_from_intseq_le (Seq.slice b 1 4) ==
    v b.[ 1 ] + pow2 64 * (nat_from_intseq_le (Seq.slice b 2 4)));
nat_from_intseq_le_slice_lemma #U64 #SEC #2 (Seq.slice b 2 4) 1;
nat_from_intseq_le_lemma0 (Seq.slice b 2 3);
assert (nat_from_intseq_le (Seq.slice b 2 4) ==
    v b.[ 2 ] + pow2 64 * (nat_from_intseq_le (Seq.slice b 3 4)));
nat_from_intseq_le_lemma0 (Seq.slice b 3 4);
assert (res == v b.[ 0 ] + pow2 64 * (v b.[ 1 ] + pow2 64 * (v b.[ 2 ] + pow2 64 * v b.[ 3 ])))
Hacl.Impl.Curve25519.Lemmas.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Impl.Curve25519.Lemmas.fst
Lib.Sequence.lseq Lib.IntTypes.uint64 Prims._assert Prims.eq2 Prims.int Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.Sequence.op_String_Access FStar.Mul.op_Star Prims.pow2 Prims.unit Lib.ByteSequence.nat_from_intseq_le_lemma0 FStar.Seq.Base.slice Lib.ByteSequence.nat_from_intseq_le Lib.ByteSequence.nat_from_intseq_le_slice_lemma Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Multiply Lib.Sequence.length Lib.IntTypes.int_t
module Hacl.Impl.Curve25519.Lemmas

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

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

val lemma_nat_from_uints64_le_4: b:lseq uint64 4 -> Lemma
  (nat_from_intseq_le b == v b.[0] + v b.[1] * pow2 64 +
    v b.[2] * pow2 64 * pow2 64 + v b.[3] * pow2 64 * pow2 64 * pow2 64)
val lemma_nat_from_uints64_le_4: b:lseq uint64 4 -> Lemma
  (nat_from_intseq_le b == v b.[0] + v b.[1] * pow2 64 +
    v b.[2] * pow2 64 * pow2 64 + v b.[3] * pow2 64 * pow2 64 * pow2 64)
b: Lib.Sequence.lseq Lib.IntTypes.uint64 4
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.ByteSequence.nat_from_intseq_le b ==
      Lib.IntTypes.v b.[ 0 ] + Lib.IntTypes.v b.[ 1 ] * Prims.pow2 64 +
      (Lib.IntTypes.v b.[ 2 ] * Prims.pow2 64) * Prims.pow2 64 +
      ((Lib.IntTypes.v b.[ 3 ] * Prims.pow2 64) * Prims.pow2 64) * Prims.pow2 64)