law mul_assoc_sym

bend-mathlib@0.8.1.0 · nat.bend:3994

import Base

3994# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
3995law mul_assoc_sym:
3996  for a: Nat
3997  for b: Nat
3998  for c: Nat
3999  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}