law from_nat_mul

import lawful-words@0.1.0.0/LAWS.bend as LAWS

import Base

128law from_nat_mul:
129  for x: Nat
130  for y: Nat
131  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}

Uses (6)

U32
Nat
Nat.mul
U32.from_nat
U32.mul
…

Used by (0)

No other definition uses this definition.