law succ_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:3956

import Base

3956# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
3957law succ_mul_sym:
3958  for n: Nat
3959  for m: Nat
3960  {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}