val lemma_mul_associate (#f:G.field) (a b c:G.felem f) : Lemma
  (fmul a (fmul b c) == fmul (fmul a b) c)
let lemma_mul_associate #f a b c =
  let pa = to_poly a in
  let pb = to_poly b in
  let pc = to_poly c in
  let m = irred_poly f in
  lemma_mul_associate pa pb pc;
  // (((a * b) % m) * c) % m
  // (a * ((b * c) % m)) % m
  PL.lemma_mod_mul_mod (pa *. pb) m pc;
  PL.lemma_mod_mul_mod (pb *. pc) m pa;
  Vale.Math.Poly2.lemma_mul_commute pa (pb *. pc);
  Vale.Math.Poly2.lemma_mul_commute pa ((pb *. pc) %. m);
  lemma_eq_to_poly (fmul a (fmul b c)) (fmul (fmul a b) c)
val lemma_mul_associate (#f:G.field) (a b c:G.felem f) : Lemma
  (fmul a (fmul b c) == fmul (fmul a b) c)
let lemma_mul_associate #f a b c =
let pa = to_poly a in
let pb = to_poly b in
let pc = to_poly c in
let m = irred_poly f in
lemma_mul_associate pa pb pc;
PL.lemma_mod_mul_mod (pa *. pb) m pc;
PL.lemma_mod_mul_mod (pb *. pc) m pa;
Vale.Math.Poly2.lemma_mul_commute pa (pb *. pc);
Vale.Math.Poly2.lemma_mul_commute pa ((pb *. pc) %. m);
lemma_eq_to_poly (fmul a (fmul b c)) (fmul (fmul a b) c)
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 Prims.unit Vale.Math.Poly2.lemma_mul_commute Vale.Math.Poly2.op_Percent_Dot Vale.Math.Poly2.op_Star_Dot Vale.Math.Poly2.Lemmas.lemma_mod_mul_mod Vale.Math.Poly2.lemma_mul_associate 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;
  ()

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

let lemma_mul_one #f a =
  let pa = to_poly a in
  let m = irred_poly f in
  lemma_mul_one pa;
  PL.lemma_mod_small pa m;
  lemma_eq_to_poly (fmul a G.one) a

let lemma_mul_commute #f a b =
  let pa = to_poly a in
  let pb = to_poly b in
  let m = irred_poly f in
  lemma_mul_commute pa pb;
  lemma_eq_to_poly (fmul a b) (fmul b a)
val lemma_mul_associate (#f:G.field) (a b c:G.felem f) : Lemma
  (fmul a (fmul b c) == fmul (fmul a b) c)
a: Spec.GaloisField.felem f -> b: Spec.GaloisField.felem f -> c: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Poly2.Galois.Lemmas.fmul a (Vale.Math.Poly2.Galois.Lemmas.fmul b c) ==
      Vale.Math.Poly2.Galois.Lemmas.fmul (Vale.Math.Poly2.Galois.Lemmas.fmul a b) c)