law mul_right_comm

bend-mathlib@0.8.1.0 · nat.bend:2159

import Base

2159# Right commutativity of multiplication: (a * b) * c = (a * c) * b.
2160law mul_right_comm:
2161  for a: Nat
2162  for b: Nat
2163  for c: Nat
2164  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}