law nat_mul_left_comm
import bend-osdev-u32@0.1.0.0/LAWS.bend as LAWSimport Base
292law nat_mul_left_comm:
293 for +x: Nat
294 for +y: Nat
295 for +z: Nat
296 {Nat.mul(x, Nat.mul(y, z)) == Nat.mul(y, Nat.mul(x, z)) : Nat}
Uses (7)
Used by (0)
No other definition uses this definition.