law mul_assoc

lawful-words@0.1.0.0 · proof_nat.bend:469

import Base

469law mul_assoc:
470  for +a: Nat
471  for +b: Nat
472  for +c: Nat
473  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}