let max = FStar.Math.Lib.max
let max =
FStar.Math.Lib.max
Vale.Math.Poly2.Galois.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.fsti.checked Spec.GaloisField.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Vale.Math.Poly2.Galois.fsti
FStar.Math.Lib.max
module Vale.Math.Poly2.Galois
open FStar.Mul
module I = Lib.IntTypes
module G = Spec.GaloisField
module P = Vale.Math.Poly2_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2
open FStar.Seq

(*
Connect Spec.GaloisField to Vale.Math.Poly2*
*)

val to_poly (#f:G.field) (e:G.felem f) : poly
val to_felem (f:G.field) (p:poly) : G.felem f

let irred_poly (f:G.field) : poly =
  let G.GF t irred = f in
  monomial (I.bits t) +. to_poly #f irred
val max : x: Prims.int -> y: Prims.int -> z: Prims.int{(x >= y ==> z = x) /\ (x < y ==> z = y)}
x: Prims.int -> y: Prims.int -> z: Prims.int{(x >= y ==> z = x) /\ (x < y ==> z = y)}