law mul_left_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4462

import Base

4462# Left commutativity of multiplication: a * (b * c) = b * (a * c), reversed to rewrite toward the simple side.
4463law mul_left_comm_sym:
4464  for a: Nat
4465  for b: Nat
4466  for c: Nat
4467  {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}