let fadd (#f:G.field) (a b:G.felem f) = G.fadd #f a b
let fadd (#f: G.field) (a b: G.felem f) =
G.fadd #f a b
Vale.Math.Poly2.Galois.Lemmas.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Galois.fsti.checked Vale.Math.Poly2.fsti.checked Spec.GaloisField.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Galois.Lemmas.fsti
Spec.GaloisField.field Spec.GaloisField.felem Spec.GaloisField.fadd
module Vale.Math.Poly2.Galois.Lemmas
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 Vale.Math.Poly2.Galois
val fadd : a: Spec.GaloisField.felem f -> b: Spec.GaloisField.felem f -> Spec.GaloisField.felem f
a: Spec.GaloisField.felem f -> b: Spec.GaloisField.felem f -> Spec.GaloisField.felem f