law nat_mul_left_comm

bend-mathlib@0.8.1.0 · algebra.bend:152

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

152# Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm).
153law nat_mul_left_comm:
154  for +a: Nat
155  for +b: Nat
156  for +c: Nat
157  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}