law mul_assoc

bend-mathlib@0.8.1.0 · nat.bend:322

import Base

322# Multiplication is associative: (a * b) * c = a * (b * c).
323law mul_assoc:
324  for a: Nat
325  for b: Nat
326  for c: Nat
327  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}