val of_nat (x:nat) : poly
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
val of_nat (x:nat) : poly
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
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_Equality Prims.int Vale.Math.Poly2_s.zero Prims.bool Prims.op_Modulus Vale.Math.Poly2.op_Plus_Dot Vale.Math.Poly2_s.one Vale.Math.Poly2_s.poly Vale.Math.Poly2_s.shift Vale.Math.Poly2.Bits.of_nat Prims.op_Division
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');
  ()
val of_nat (x:nat) : poly
x: Prims.nat -> Vale.Math.Poly2_s.poly