val index_be_to_n' (b: bytes) (i: nat)
    : Lemma (requires (i < S.length b))
      (ensures (U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8))
      (decreases (S.length b))
let rec index_be_to_n'
  (b: bytes)
  (i: nat)
: Lemma
  (requires (
    i < S.length b
  ))
  (ensures (
    U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8
  ))
  (decreases (S.length b))
= reveal_be_to_n b;
  if i = S.length b - 1
  then ()
  else begin
    let l = S.length b in
    let l' = l - 1 in
    let b' = S.slice b 0 l' in
    index_be_to_n' b' i;
    assert (S.index b i == S.index b' i);
    let open FStar.Math.Lemmas in
    let x = be_to_n b in
    let x' = be_to_n b' in
    assert (U8.v (S.index b i) == x' / pow2 (8 * (l' - 1 - i)) % pow2 8);
    let y = (U8.v (S.last b) + pow2 8 * x') / pow2 (8 * (l - 1 - i)) % pow2 8 in
    pow2_plus 8 (8 * (l' - 1 - i));
    division_multiplication_lemma (U8.v (S.last b) + pow2 8 * x') (pow2 8) (pow2 (8 * (l' - 1 - i)));
    assert (pow2 8 * x' == x' * pow2 8);
    division_addition_lemma (U8.v (S.last b)) (pow2 8) x';
    small_division_lemma_1 (U8.v (S.last b)) (pow2 8);
    assert (y == x' / pow2 (8 * (l' - 1 - i)) % pow2 8)
  end
val index_be_to_n' (b: bytes) (i: nat)
    : Lemma (requires (i < S.length b))
      (ensures (U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8))
      (decreases (S.length b))
let rec index_be_to_n' (b: bytes) (i: nat)
    : Lemma (requires (i < S.length b))
      (ensures (U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8))
      (decreases (S.length b)) =
reveal_be_to_n b;
if i = S.length b - 1
then ()
else
  let l = S.length b in
  let l' = l - 1 in
  let b' = S.slice b 0 l' in
  index_be_to_n' b' i;
  assert (S.index b i == S.index b' i);
  let open FStar.Math.Lemmas in
  let x = be_to_n b in
  let x' = be_to_n b' in
  assert (U8.v (S.index b i) == x' / pow2 (8 * (l' - 1 - i)) % pow2 8);
  let y = (U8.v (S.last b) + pow2 8 * x') / pow2 (8 * (l - 1 - i)) % pow2 8 in
  pow2_plus 8 (8 * (l' - 1 - i));
  division_multiplication_lemma (U8.v (S.last b) + pow2 8 * x') (pow2 8) (pow2 (8 * (l' - 1 - i)));
  assert (pow2 8 * x' == x' * pow2 8);
  division_addition_lemma (U8.v (S.last b)) (pow2 8) x';
  small_division_lemma_1 (U8.v (S.last b)) (pow2 8);
  assert (y == x' / pow2 (8 * (l' - 1 - i)) % pow2 8)
LowParse.Endianness.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
LowParse.Endianness.fst
FStar.Endianness.bytes Prims.nat Prims.op_Equality Prims.int Prims.op_Subtraction FStar.Seq.Base.length FStar.UInt8.t Prims.bool Prims._assert Prims.eq2 Prims.op_Modulus Prims.op_Division Prims.pow2 FStar.Mul.op_Star Prims.unit FStar.Math.Lemmas.small_division_lemma_1 FStar.UInt8.v FStar.Seq.Properties.last FStar.Math.Lemmas.division_addition_lemma FStar.Math.Lemmas.division_multiplication_lemma Prims.op_Addition FStar.Math.Lemmas.pow2_plus FStar.Seq.Base.index FStar.Endianness.be_to_n LowParse.Endianness.index_be_to_n' FStar.Seq.Base.seq FStar.Seq.Base.slice FStar.Endianness.reveal_be_to_n Prims.b2t Prims.op_LessThan Prims.squash Prims.Nil FStar.Pervasives.pattern
module LowParse.Endianness

let rec index_be_to_n'
  (b: bytes)
  (i: nat)
: Lemma
  (requires (
    i < S.length b
  ))
  (ensures (
    U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8
  ))
val index_be_to_n' (b: bytes) (i: nat)
    : Lemma (requires (i < S.length b))
      (ensures (U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8))
      (decreases (S.length b))
b: FStar.Endianness.bytes -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i < FStar.Seq.Base.length b)
      (ensures
        FStar.UInt8.v (FStar.Seq.Base.index b i) ==
        FStar.Endianness.be_to_n b / Prims.pow2 (8 * (FStar.Seq.Base.length b - 1 - i)) %
        Prims.pow2 8)
      (decreases FStar.Seq.Base.length b)