1	# GF(2^m) (gfm.bend), for every field and every input: a product is the
2	# product of its factors' elements (Gfm.elt), so a factor may be reduced
3	# first. In a pair of its own, with no table proofs, so that a proof
4	# elsewhere (rs) can use it without importing PROOF.bend.
5	import Base
6	import ./gfm.bend as M
7	
8	law gfm_mul_elt:
9	  for +f: M.GfmField
10	  for +a: U32
11	  for +b: U32
12	  {M.Gfm.mul(f, M.Gfm.elt(f, a), b) == M.Gfm.mul(f, a, b) : U32}