val lemma_of_to_vec_zero (i n: nat)
    : Lemma (requires i < n)
      (ensures index (to_vec #n 0) i == false)
      [SMTPat (index (to_vec #n 0) i)]
let rec lemma_of_to_vec_zero (i:nat) (n:nat) : Lemma
  (requires i < n)
  (ensures index (to_vec #n 0) i == false)
  [SMTPat (index (to_vec #n 0) i)]
  =
  if i + 1 < n then lemma_of_to_vec_zero i (n - 1)
val lemma_of_to_vec_zero (i n: nat)
    : Lemma (requires i < n)
      (ensures index (to_vec #n 0) i == false)
      [SMTPat (index (to_vec #n 0) i)]
let rec lemma_of_to_vec_zero (i n: nat)
    : Lemma (requires i < n)
      (ensures index (to_vec #n 0) i == false)
      [SMTPat (index (to_vec #n 0) i)] =
if i + 1 < n then lemma_of_to_vec_zero i (n - 1)
Vale.Math.Poly2.Bits.fst.checked
Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Math.Poly2.Bits.fst
Prims.nat Prims.op_LessThan Prims.op_Addition Vale.Math.Poly2.Bits.lemma_of_to_vec_zero Prims.op_Subtraction Prims.bool Prims.unit Prims.b2t Prims.squash Prims.eq2 FStar.Seq.Base.index FStar.UInt.to_vec Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module Vale.Math.Poly2.Bits
open FStar.Mul
open Vale.Arch.TypesNative

let lemma_to_of_uint n u =
  let a = of_uint n u in
  let u' = to_uint n a in
  lemma_index a;
  lemma_reverse_define_all ();
  let s = UInt.to_vec #n u in
  let s' = UInt.to_vec #n u' in
  assert (equal s s');
  ()

let rec of_nat x =
  if x = 0 then zero
  else
    let p = shift (of_nat (x / 2)) 1 in
    if x % 2 = 0 then p else p +. one

let rec lemma_of_to_vec_zero (i:nat) (n:nat) : Lemma
  (requires i < n)
  (ensures index (to_vec #n 0) i == false)
  [SMTPat (index (to_vec #n 0) i)]
val lemma_of_to_vec_zero (i n: nat)
    : Lemma (requires i < n)
      (ensures index (to_vec #n 0) i == false)
      [SMTPat (index (to_vec #n 0) i)]
i: Prims.nat -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires i < n)
      (ensures FStar.Seq.Base.index (FStar.UInt.to_vec 0) i == false)
      [SMTPat (FStar.Seq.Base.index (FStar.UInt.to_vec 0) i)]