val lemma_eq_to_poly (#f:G.field) (a b:G.felem f) : Lemma
  (requires to_poly a == to_poly b)
  (ensures a == b)
let lemma_eq_to_poly #f a b =
  lemma_felem_poly a;
  lemma_felem_poly b;
  ()
val lemma_eq_to_poly (#f:G.field) (a b:G.felem f) : Lemma
  (requires to_poly a == to_poly b)
  (ensures a == b)
let lemma_eq_to_poly #f a b =
lemma_felem_poly a;
lemma_felem_poly b;
()
Vale.Math.Poly2.Galois.Lemmas.fst.checked
Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Galois.Lemmas.fst
Spec.GaloisField.field Spec.GaloisField.felem Prims.unit Vale.Math.Poly2.Galois.lemma_felem_poly
module Vale.Math.Poly2.Galois.Lemmas
open FStar.Mul
module PL = Vale.Math.Poly2.Lemmas
val lemma_eq_to_poly (#f:G.field) (a b:G.felem f) : Lemma
  (requires to_poly a == to_poly b)
  (ensures a == b)
a: Spec.GaloisField.felem f -> b: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
      (requires Vale.Math.Poly2.Galois.to_poly a == Vale.Math.Poly2.Galois.to_poly b)
      (ensures a == b)