law mul_left_comm

bend-mathlib@0.8.1.0 · nat.bend:2144

import Base

2144# Left commutativity of multiplication: a * (b * c) = b * (a * c).
2145law mul_left_comm:
2146  for a: Nat
2147  for b: Nat
2148  for c: Nat
2149  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}