val lemma_mul_zero (#f:G.field) (a:G.felem f) : Lemma (fmul a G.zero == G.zero)
let lemma_mul_zero #f a =
  let pa = to_poly a in
  let m = irred_poly f in
  lemma_mul_zero pa;
  PL.lemma_mod_small zero m;
  lemma_eq_to_poly (fmul a G.zero) G.zero
val lemma_mul_zero (#f:G.field) (a:G.felem f) : Lemma (fmul a G.zero == G.zero)
let lemma_mul_zero #f a =
let pa = to_poly a in
let m = irred_poly f in
lemma_mul_zero pa;
PL.lemma_mod_small zero m;
lemma_eq_to_poly (fmul a G.zero) G.zero
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 Vale.Math.Poly2.Galois.Lemmas.lemma_eq_to_poly Vale.Math.Poly2.Galois.Lemmas.fmul Spec.GaloisField.zero Prims.unit Vale.Math.Poly2.Lemmas.lemma_mod_small Vale.Math.Poly2_s.zero Vale.Math.Poly2.lemma_mul_zero Vale.Math.Poly2_s.poly Vale.Math.Poly2.Galois.irred_poly Vale.Math.Poly2.Galois.to_poly
module Vale.Math.Poly2.Galois.Lemmas
open FStar.Mul
module PL = Vale.Math.Poly2.Lemmas

let lemma_eq_to_poly #f a b =
  lemma_felem_poly a;
  lemma_felem_poly b;
  ()
val lemma_mul_zero (#f:G.field) (a:G.felem f) : Lemma (fmul a G.zero == G.zero)
a: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
    (ensures Vale.Math.Poly2.Galois.Lemmas.fmul a Spec.GaloisField.zero == Spec.GaloisField.zero)