law mul_comm

bend-mathlib@0.8.1.0 · nat.bend:271

import Base

271# Multiplication is commutative: n * m = m * n.
272law mul_comm:
273  for n: Nat
274  for m: Nat
275  {Nat.mul(n, m) == Nat.mul(m, n) : Nat}