val lemma_to_of_uint (n:pos) (u:uint_t n) : Lemma
  (ensures to_uint n (of_uint n u) == u)
  [SMTPat (to_uint n (of_uint n u))]
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');
  ()
val lemma_to_of_uint (n:pos) (u:uint_t n) : Lemma
  (ensures to_uint n (of_uint n u) == u)
  [SMTPat (to_uint n (of_uint n u))]
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');
()
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.pos FStar.UInt.uint_t Prims.unit Prims._assert FStar.Seq.Base.equal Prims.bool FStar.BitVector.bv_t FStar.UInt.to_vec Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_index Vale.Math.Poly2.Bits_s.to_uint Vale.Math.Poly2_s.poly Vale.Math.Poly2.Bits_s.of_uint
module Vale.Math.Poly2.Bits
open FStar.Mul
open Vale.Arch.TypesNative
val lemma_to_of_uint (n:pos) (u:uint_t n) : Lemma
  (ensures to_uint n (of_uint n u) == u)
  [SMTPat (to_uint n (of_uint n u))]
n: Prims.pos -> u3: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma
      (ensures Vale.Math.Poly2.Bits_s.to_uint n (Vale.Math.Poly2.Bits_s.of_uint n u3) == u3)
      [SMTPat (Vale.Math.Poly2.Bits_s.to_uint n (Vale.Math.Poly2.Bits_s.of_uint n u3))]