law nat_mul_assoc

lawful-words@0.1.0.0 · LAWS.bend:526

import Base

526law nat_mul_assoc:
527  for a: Nat
528  for b: Nat
529  for c: Nat
530  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}