val lemma_to_poly_degree (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures degree (to_poly e) < I.bits f.G.t)
  [SMTPat (to_poly e)]
let lemma_to_poly_degree #f e =
  reveal_defs ()
val lemma_to_poly_degree (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures degree (to_poly e) < I.bits f.G.t)
  [SMTPat (to_poly e)]
let lemma_to_poly_degree #f e =
reveal_defs ()
Vale.Math.Poly2.Galois.fst.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Galois.IntTypes.fsti.checked Vale.Math.Poly2.Defs_s.fst.checked prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.Compatibility.fst.checked Lib.IntTypes.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Galois.fst
Spec.GaloisField.field Spec.GaloisField.felem Vale.Math.Poly2_s.reveal_defs Prims.unit
module Vale.Math.Poly2.Galois
open FStar.Mul

module U = FStar.UInt
module PL = Vale.Math.Poly2.Lemmas
module D = Vale.Math.Poly2.Defs_s
//module PD = Vale.Math.Poly2.Defs
module GI = Vale.Math.Poly2.Galois.IntTypes

// recursive definitions of from_vec/to_vec are prone to matching loops, so use no fuel from here on
#reset-options "--max_fuel 0 --max_ifuel 0"

let to_poly #f e =
  let G.GF t irred = f in
  let n = I.bits t in
  reverse (of_seq (U.to_vec #n (I.v e))) (n - 1)

let to_felem f p =
  let G.GF t irred = f in
  let n = I.bits t in
  let p = reverse p (n - 1) in
  Lib.IntTypes.Compatibility.nat_to_uint (U.from_vec #n (to_seq p n))
val lemma_to_poly_degree (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures degree (to_poly e) < I.bits f.G.t)
  [SMTPat (to_poly e)]
e: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.Math.Poly2_s.degree (Vale.Math.Poly2.Galois.to_poly e) < Lib.IntTypes.bits (GF?.t f))
      [SMTPat (Vale.Math.Poly2.Galois.to_poly e)]