law succ_mul

bend-mathlib@0.8.1.0 · nat.bend:261

import Base

261# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
262law succ_mul:
263  for n: Nat
264  for m: Nat
265  {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}