law from_nat_mul

lawful-words@0.1.0.0 · proof_u32.bend:491

import Base

491law from_nat_mul:
492  for +x: Nat
493  for +y: Nat
494  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}