law mul_succ

bend-mathlib@0.8.1.0 · nat.bend:244

import Base

244# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
245law mul_succ:
246  for n: Nat
247  for m: Nat
248  {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}