law nat_mul_right_comm

bend-mathlib@0.8.1.0 · algebra.bend:162

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

162# Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm).
163law nat_mul_right_comm:
164  for +a: Nat
165  for +b: Nat
166  for +c: Nat
167  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}