law mul_right_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4472

import Base

4472# Right commutativity of multiplication: (a * b) * c = (a * c) * b, reversed to rewrite toward the simple side.
4473law mul_right_comm_sym:
4474  for a: Nat
4475  for b: Nat
4476  for c: Nat
4477  {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}