val lemma_irred_degree (f:G.field) : Lemma
  (requires True)
  (ensures degree (irred_poly f) == I.bits f.G.t)
  [SMTPat (irred_poly f)]
let lemma_irred_degree f =
  let G.GF t irred = f in
  let n = I.bits t in
  PL.lemma_index_all ();
  PL.lemma_monomial_define n;
  PL.lemma_add_define_all ();
  PL.lemma_degree_is (irred_poly f) n;
  ()
val lemma_irred_degree (f:G.field) : Lemma
  (requires True)
  (ensures degree (irred_poly f) == I.bits f.G.t)
  [SMTPat (irred_poly f)]
let lemma_irred_degree f =
let G.GF t irred = f in
let n = I.bits t in
PL.lemma_index_all ();
PL.lemma_monomial_define n;
PL.lemma_add_define_all ();
PL.lemma_degree_is (irred_poly f) n;
()
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 Lib.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.op_disEquality Lib.IntTypes.U1 Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.unit Vale.Math.Poly2.Lemmas.lemma_degree_is Vale.Math.Poly2.Galois.irred_poly Vale.Math.Poly2.Lemmas.lemma_add_define_all Vale.Math.Poly2.Lemmas.lemma_monomial_define Vale.Math.Poly2.Lemmas.lemma_index_all Prims.int Lib.IntTypes.bits
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))

let lemma_to_poly_degree #f e =
  reveal_defs ()
val lemma_irred_degree (f:G.field) : Lemma
  (requires True)
  (ensures degree (irred_poly f) == I.bits f.G.t)
  [SMTPat (irred_poly f)]
f: Spec.GaloisField.field
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.Math.Poly2_s.degree (Vale.Math.Poly2.Galois.irred_poly f) ==
        Lib.IntTypes.bits (GF?.t f)) [SMTPat (Vale.Math.Poly2.Galois.irred_poly f)]