law mul_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:3965

import Base

3965# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
3966law mul_comm_sym:
3967  for n: Nat
3968  for m: Nat
3969  {Nat.mul(m, n) == Nat.mul(n, m) : Nat}